SMT-Constrained Symbolic Execution for Eclipse CDT/Codan
作者： Andreas Ibing
DOI: 10.1007/978-3-319-05032-4_9
关键词: Solver 、 Test suite 、 Eclipse 、 Satisfiability modulo theories 、 Interface (Java) 、 Programming language 、 Integer (computer science) 、 Computer science 、 Symbolic execution 、 Parallel computing 、 Context (language use)
摘要: This paper presents a symbolic execution plug-in extension for Eclipse CDT/Codan, which serves to reason about satisfiable paths of C programs. Programs are translated into the SMT-LIB sublogic arrays, uninterpreted functions and nonlinear integer real arithmetic (AUFNIRA), path satisfiability is automatically examined with an SMT solver. The presented can serve as basis path-sensitive static bug detection bounded or unrestricted context, where presence bugs decided An interface provides notifications context information checker classes. With buffer bound shown capable accurately detecting currently 36 39 flow variants NSA's Juliet test suite analyzers.
springer.com
acm.org 
sci-hub.st 参考文章(25)
Daniel Le Berre, Anne Parrain, The SAT4J library, Release 2.2, System Description Journal on Satisfiability, Boolean Modeling and Computation. ,vol. 7, pp. 59- 64 ,(2010) , 10.3233/SAT190075
Uday P. Khedker, Data Flow Analysis. The Compiler Design Handbook. pp. 1- 59 ,(2002)
Peter F. Patel-Schneider, DLP System Description. Description Logics. ,(1998)
Micha Sharir, A Pnueli, Two approaches to interprocedural data flow analysis ,(2011)
Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, Roberto Sebastiani, The MathSAT5 SMT solver tools and algorithms for construction and analysis of systems. pp. 93- 107 ,(2013) , 10.1007/978-3-642-36742-7_7
Frank Tip, A survey of program slicing techniques. Journal of Programming Languages. ,vol. 3, ,(1995)
Uday Khedker, Bageshri Karkare, Amitabha Sanyal, Data Flow Analysis: Theory and Practice ,(2009)
John Harrison, Handbook of Practical Logic and Automated Reasoning ,(2009)
Cristian Cadar, Daniel Dunbar, Dawson Engler, KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs operating systems design and implementation. pp. 209- 224 ,(2008) , 10.5555/1855741.1855756
Yichen Xie, Alex Aiken, Scalable error detection using boolean satisfiability symposium on principles of programming languages. ,vol. 40, pp. 351- 363 ,(2005) , 10.1145/1040305.1040334