Precise and progressing compositional symbolic execution

Given a program and an assertion in that program, determining whether 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. It enjoys the following two interesting properties. First, symbolic execution is 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 is 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 semi-decision procedure. Recently, compositional symbolic execution algorithms have been proposed. They improve 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 hence a semi-decision procedure), and reports on the implementation of one such algorithm.nrpages: 22status: publishe