Abstract:

Most static program analysis techniques do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties, fail to verify properties, or check properties under certain unsound assumptions, such as the absence of arithmetic overflow. In the first part of the talk, I will present a technique to complement partial verification results by automatic test case generation. In contrast to existing work, our technique supports the common case that the verification results are based on unsound assumptions. We annotate programs to reflect which executions have been verified, and under which assumptions. These annotations are then used to guide dynamic symbolic execution toward unverified program executions, leading to smaller and more effective test suites.

In the second part of the talk, I will describe a new program simplification technique, called program trimming. Program trimming is a program pre-processing step to remove execution paths while retaining equi-safety (that is, the generated program has a bug if and only if the original program has a bug). Since many program analyzers are sensitive to the number of execution paths, program trimming has the potential to improve their effectiveness.  I will show that program trimming has a considerable positive impact on the effectiveness of two program analysis techniques, abstract interpretation and dynamic symbolic execution.