On Automation Of Ctl* Verification For Infinite-State Systems
COMPUTER AIDED VERIFICATION, PT I(2015)
摘要
In this paper we introduce the first known fully automated tool for symbolically proving CTL* properties of (infinite-state) integer programs. The method uses an internal encoding which facilitates reasoning about the subtle interplay between the nesting of path and state temporal operators that occurs within CTL* proofs. A precondition synthesis strategy is then used over a program transformation which trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We show the viability of our approach in practice using examples drawn from device drivers and various industrial examples.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络