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.
- 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]
The Tandem project has been funded by ETH Zurich.