Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
复制标题
使用循环证明自动验证指针程序的时间属性
DOI：
10.1007/s10817-019-09532-0
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
J. Brotherston
中科院分区：
文献类型：
--
作者：
Gadi Tellez;J. Brotherston
在本文中，我们调查了堆意见程序的时间属性的自动验证。我们提出了一种基于循环证明的演绎推理方法。我们的证明系统中的判断断言，一个程序在记忆状态主张上具有一定的时间属性，并以用户定义的归纳谓词编写，而系统的证明规则则展现了时间模式和谓词定义以及象征性地执行程序。像往常一样，我们系统中的循环证明具有有限的证明图，但具有自然，可决定性的声音条件，通过无限下降编码一种证明形式。我们提出了一个量身定制的证明系统，该系统是为了证明非确定性指针程序的CTL属性，然后调整此系统以处理公平的执行条件。我们显示系统的两个版本都是合理的，并提供了骑自行车的定理摊贩中每个版本的实现，并产生了一个自动化工具，该工具能够自动发现指针程序的（公平）时间属性的证明。对我们工具的实验评估表明我们的方法是可行的，并为传统模型检查技术提供了有趣的替代方法。
In this article, we investigate the automated verification of temporal properties of heap-aware programs. We propose a deductive reasoning approach based on cyclic proof. Judgements in our proof system assert that a program has a certain temporal property over memory state assertions, written in separation logic with user-defined inductive predicates, while the proof rules of the system unfold temporal modalities and predicate definitions as well as symbolically executing programs. Cyclic proofs in our system are, as usual, finite proof graphs subject to a natural, decidable soundness condition, encoding a form of proof by infinite descent. We present a proof system tailored to proving CTL properties of nondeterministic pointer programs, and then adapt this system to handle fair execution conditions. We show both versions of the system to be sound, and provide an implementation of each in the Cyclist theorem prover, yielding an automated tool that is capable of automatically discovering proofs of (fair) temporal properties of pointer programs. Experimental evaluation of our tool indicates that our approach is viable, and offers an interesting alternative to traditional model checking techniques.