Tandem
Tandem applies static program analyzers to check program properties. In practice, these verification results are often partial because the analyzers do not check certain properties or make unjustified assumptions. The main idea of this project is to direct automatic testing tools such that they target specifically the executions and properties not checked soundly by a static analysis.
Even though static analyzers effectively detect software errors, they cannot replace or significantly reduce the test effort. Practical tools for mainstream languages make a number of compromises to increase automation, reduce the annotation overhead for the programmer, reduce the number of false positives, and improve performance. These compromises include not checking certain properties (e.g., termination), making implicit assumptions (e.g., integer values), and unsoundness (for instance, considering only a fixed number of loop iterations).
Despite these limitations, static analyzers are useful because they find real errors in real code. However, as a result of these limitations, it is not clear what guarantees a static analysis actually provides and how to use testing to check those properties that are not soundly verified by a static analysis. Consequently, software engineers need to unit test their programs as if static analyses were not applied, which is inefficient and requires large test suites.
Tandem suggests a tool architecture that allows software engineers to combine multiple, complementary static analyzers that check different properties and assumptions, and to complement static program analysis by automatic specification-based test case generation to cover those executions and properties that have not been checked statically. Our architecture makes explicit which properties have been checked statically, and under which assumptions. Therefore, the guarantees provided by static analyzers are documented precisely and can be used to target testing toward those properties not verified yet, leading to smaller and more effective test suites.
Project Members
The project has been completed. Please contact Peter Müller in case of questions or comments.
Key Publications
- M. Christakis and P. Müller and V. Wüstholz: Guiding Dynamic Symbolic Execution toward Unverified Program Executions
International Conference on Software Engineering (ICSE), 2016. To appear. [PDF] [BIB]
- M. Christakis, P. Müller, and V. Wüstholz: An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer
Verification, Model Checking, and Abstract Interpretation (VMCAI), 2015. [PDF] [BIB] - M. Christakis, P. Emmisberger, and P. Müller: Dynamic Test Generation with Static Fields and Initializers
Runtime Verification (RV), 2014. [PDF] [BIB] - M. Christakis, P. Müller, and V. Wüstholz: Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations
Software Engineering and Formal Methods (SEFM), 2014. [PDF] [BIB] - M. Christakis, P. Müller, and V. Wüstholz: Collaborative Verification and Testing with Explicit Assumptions
Formal Methods (FM), 2012. [PDF] [BIB]
Acknowledgments
The Tandem project has been funded by ETH Zurich.