Modular verification of code with SAT
Greg Dennis, Felix Sheng-Ho Chang, Daniel Jackson · 2006
An approach is described for checking the methods of a class against a full specification. It shares with traditional model checking the idea of exhausting the entire space of executions within some finite bounds, and with traditional verification the idea of modular analysis, in which a method is analyzed, in isolation, for all possible calling contexts.The analysis involves an automatic two-phase reduction: first, to an intermediate form in relational logic (using a new encoding described here), and second, to a boolean formula (using existing techniques), which is then handed to an off the shelf SAT solver.A variety of implementations of the Java Collections Framework's List interface were checked against existing JML specifications. The analysis revealed bugs in the implementations, as well as errors in the specifications themselves.