Interpolation-based software verification with WOLVERINE
作者： Daniel Kroening , Georg Weissenbacher
DOI: 10.1007/978-3-642-22110-1_45
关键词:
摘要: Wolverine is a software verification tool using Craig interpolation to compute invariants of ANSI-C and C++ programs. The an implementation the lazy abstraction approach, generating reachability tree by unwinding transition relation input program annotating its nodes with interpolants representing safe states. features built-in interpolating decision procedure for equality logic uninterpreted functions which provides limited support bit-vector operations. In addition, it API enabling integration other procedures, making valuable source benchmarks allowing take advantage continuous performance improvements SMT solvers. We evaluate comparing predicate abstraction-based verifier SATABS on number conditions Linux device drivers.
springer.com
kroening.com 参考文章(23)
Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher, Model checking concurrent linux device drivers automated software engineering. pp. 501- 504 ,(2007) , 10.1145/1321631.1321719
Vijay D'Silva, Daniel Kroening, Georg Weissenbacher, A Survey of Automated Techniques for Formal Software Verification IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. ,vol. 27, pp. 1165- 1178 ,(2008) , 10.1109/TCAD.2008.923410
Ranjit Jhala, Rupak Majumdar, Software model checking ACM Computing Surveys. ,vol. 41, pp. 1- 54 ,(2009) , 10.1145/1592434.1592438
Georg Weissenbacher, Daniel Kroening, Lifting Propositional Interpolants to the Word-Level formal methods in computer-aided design. pp. 85- 89 ,(2007) , 10.1109/FMCAD.2007.31
Thomas Ball, Byron Cook, Vladimir Levin, Sriram K. Rajamani, SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft integrated formal methods. pp. 1- 20 ,(2004) , 10.1007/978-3-540-24756-2_1
Edmund Clarke, Daniel Kroening, Flavio Lerda, A Tool for Checking ANSI-C Programs tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 168- 176 ,(2004) , 10.1007/978-3-540-24730-2_15
Roberto Bruttomesso, Edgar Pek, Natasha Sharygina, Aliaksei Tsitovich, The OpenSMT solver tools and algorithms for construction and analysis of systems. pp. 150- 153 ,(2010) , 10.1007/978-3-642-12002-2_12
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan, Abstractions from proofs symposium on principles of programming languages. ,vol. 49, pp. 232- 244 ,(2004) , 10.1145/2641638.2641655
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith, Counterexample-guided abstraction refinement international symposium on temporal representation and reasoning. ,vol. 1855, pp. 154- 169 ,(2003) , 10.1007/10722167_15
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski, Nested interpolants Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '10. pp. 471- 482 ,(2010) , 10.1145/1706299.1706353