Checking Large Programs Against Structural Properties
The aim of this project is to provide a scalable method to check programs against user-provided properties. We particularly target structural properties, i.e., properties that constrain the configuration of the heap. The analysis is modular and uses the specifications of the called procedures as surrogates for their code. These specifications however, are not provided by the user; they are inferred from the code automatically as needed.
Our analysis is based on a technique known as "counterexample-guided abstraction refinement". It starts with an abstraction of the program in which each procedure call is replaced with a rough initial specification that over-approximates its effect. The specifications are then iteratively refined in response to spurious counterexamples. Therefore, only as much information about a procedure is used as is necessary to analyze its caller. When the analysis terminates, the remaining counterexample is guaranteed not to be spurious, but because the heap is finitized, absence of a counterexample does not constitute proof.
Karun is an implementation of this framework that checks Java programs against properties expressed in Alloy with respect to a finite heap. It translates both the abstract program and the given property to a boolean formula and solves it using the ZChaff SAT solver. New specifications are then inferred from a proof of unsatisfiability generated by ZChaff.