Week6 关于我摸鱼的第六次研究生组会

汇报内容

1、汇报论文《Predicate Abstraction for Program Verification Safety and Termination》

本周阅读了对于程序验证的安全性和终止性的谓词抽象，论文表达了程序正确性属性包含两种：safety安全性（即错误状态不可达）和termination终止。引入两个概念，谓词抽象和反例引导抽象精化，我认为这个与上次老师讲述的refinement相关。论文首先介绍了一个类似的状态迁移系统，引入了V、PC、字母表等符号，其中Φ表达可达的状态集合，pesai表达可达的状态对，其中论文指出安全性可以用状态的可达描述，终止性可以用状态对的可达进行描述。

即程序安全Φreach=字母表/Φerr，其中Φreach是通过有限次迭代进行构造。接着引入程序P是可终止的，即当析取n个well-founded关系是转移不变量，Ψreach。。。Ψ1.。。Ψ2.。。Ψn，其中用有限数目的有充分的基础关系的并构成转移不变量，其中这个是事实，依赖于拉姆齐定理。然后论文通过归纳的方法来描述正确性，引入post后置函数，函数作用应该是与TS的post一致。即（。。。。），其中算法的终止性最后任何一步应用都不会产生任何额外的析取，因此Φreach是上述的析取。同理，引入（。）的关系成分函数来定义终止。程序终止：当且仅当二元关系pP交Φreach是well-founded，归纳转移不变量Ψ包含程序转移关系对可达状态的限制，以及is closed在程序转化关系下的关系组合。计算可达程序状态集合的迭代函数在多数不会终止（终止条件是迭代不会增加新的析取）。接着定义了一个带#的操作来解决无限循环迭代的问题，上线为2^n次，函数aafa（Φ）=合取{P属于Preds｜Φ｜=p}。「接着省略大部分内容和中间过程」。

反例引导精化：refinement=>将一定量的程序path作为主要信息来源=>证明这些足够的路径表示程序正确。核心算法：