Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers
Verified Software: Theories, Tools and Experiments - 6th International Conference, VSTTE 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers
复制标题
验证软件：理论、工具和实验 - 第六届国际会议，VSTTE 2014，奥地利维也纳，2014 年 7 月 17-18 日，修订后的精选论文
DOI：
10.1007/978-3-319-12154-3_12
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Freitas L
中科院分区：
文献类型：
--
作者：
Freitas L
现代定理证明器可以履行在使用形式方法（FM）时产生的很大一部分证明义务（PO）。不幸的是，剩余PO需要繁琐的手动指导。从积极的一面来看，这些“困难”的PO往往属于家庭，每个家庭只需要几个关键的想法来解锁。本文概述了一个系统，可以减少FM证明的负担，通过识别和表征的方式放电PO的一个家庭，通过跟踪家庭的一个成员的交互式证明。这打开了捕获想法的可能性-表示为证明策略-从专家和/或最大限度地重复使用的想法后，改变定义。所提出的系统必须存储丰富的元信息的结构，这可以对以前学习的策略相匹配，或可以用于构建新的策略的基础上专家的指导。
Modern theorem provers can discharge a significant proportion of Proof Obligation (POs) that arise in the use of Formal Method (FMs). Unfortunately, the residual POs require tedious manual guidance. On the positive side, these “difficult” POs tend to fall into families each of which requires only a few key ideas to unlock. This paper outlines a system that can lessen the burden of FM proofs by identifying and characterising ways of discharging POs of a family by tracking an interactive proof of one member of the family. This opens the possibility of capturing ideas — represented as proofstrategies— from an expert and/or maximising reuse of ideas after changes to definitions. The proposed system has to store a wealth of meta-information about conjectures, which can be matched against previously learned strategies, or can be used to construct new strategies based on expert guidance.