Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement
作者： Thomas Ball , Byron Cook , Shuvendu K. Lahiri , Lintao Zhang
DOI: 10.1007/978-3-540-27813-9_36
关键词:
摘要: Counterexample-driven abstraction refinement is an automatic process that produces abstract models of finite and infinite-state systems. When this applied to software, theorem prover for quantifier-free first-order logic helps determine the feasibility program paths refine abstraction. In paper we report on a fast, lightweight, called Zapato which have built specifically solve queries produced during process.
springer.com
springerlink.com
core.ac.uk 参考文章(7)
Sriram K. Rajamani, Thomas Ball, Generating Abstract Explanations of Spurious Counterexamples in C Programs pp. 15- ,(2002)
Cormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe, Theorem Proving Using Lazy Proof Explication computer aided verification. pp. 355- 367 ,(2003) , 10.1007/978-3-540-45069-6_34
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Thomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani, Refining Approximations in Software Predicate Abstraction tools and algorithms for construction and analysis of systems. pp. 388- 403 ,(2004) , 10.1007/978-3-540-24730-2_30
Shuvendu K. Lahiri, Randal E. Bryant, Byron Cook, A Symbolic Approach to Predicate Abstraction computer aided verification. pp. 141- 153 ,(2003) , 10.1007/978-3-540-45069-6_15
Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani, Automatic predicate abstraction of C programs ACM SIGPLAN Notices. ,vol. 47, pp. 37- 47 ,(2012) , 10.1145/2442776.2442783
Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani, Automatic predicate abstraction of C programs Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation - PLDI '01. ,(2001) , 10.1145/378795.378846