Theoretical Aspects of Compositional Symbolic Execution

7 years 10 months ago
Theoretical Aspects of Compositional Symbolic Execution
Given a program and an assertion in that program, determining if the assertion can fail is one of the key applications of program analysis. Symbolic execution is a well-known technique for finding such assertion violations that can enjoy the following two interesting properties. First, symbolic execution can be precise: if it reports that an assertion can fail, then there is an execution of the program that will make the assertion fail. Second, it can be progressing: if there is an execution that makes the assertion fail, it will eventually be found. A symbolic execution algorithm that is both precise and progressing is a semidecision procedure. Recently, compositional symbolic execution has been proposed. It improves scalability by analyzing each execution path of each method only once. However, proving precision and progress is more challenging for these compositional algorithms. This paper investigates under what conditions a compositional algorithm is precise and progressing (and ...
Dries Vanoverberghe, Frank Piessens
Added 28 Aug 2011
Updated 28 Aug 2011
Type Journal
Year 2011
Where FASE
Authors Dries Vanoverberghe, Frank Piessens
Comments (0)