Synthesizing Parameterized Unit Tests to Detect Object Invariant Violations

Automatic test case generation techniques rely on a description of the input data that the unit under test is intended to handle. For heap data structures, such a description is typically expressed as some form of object invariant. If a program may create structures that violate the invariant, the test data generated using the invariant systematically ignores possible inputs and, thus, potentially misses bugs. In this paper, we present a technique that detects violations of object invariants. We describe three scenarios in which traditional invariant checking may miss such violations. Based on templates that capture these scenarios, we synthesize parameterized unit tests that are likely to violate invariants, and use dynamic symbolic execution to generate inputs to the synthesized tests. We have implemented our technique as an extension to Pex and detected a significant number of invariant violations in real applications.