This paper explores the idea of augmenting traditional model checkers with the expressiveness of a declarative, relational language. The goal is to enable programmers to write very intuitive and compact specifications, in order to allow the automatic verification of more complicated software systems. The key idea is that many structural operations (common in object-oriented programs) can be easily described using relations and relational operators, while other operations are best described using the primitive data types and their operations (such as simple arithmetic operations on numbers). By allowing a mixture of both, and by allowing parts of the model to be described declaratively rather than imperatively, the programmer has the freedom to model each part of the system differently, using the most intuitive and simple constructs. We built a BDD-based model checker for the language, and successfully verified a straightforward model of the dependency algorithm in Apache Ant for up to 5 nodes.

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.

This paper introduces a new specification style for processor microarchitectures. Our goal is to produce very simple, compact, but cycle-accurate descriptions, in order to enable early exploration of different microarchitectures and their performance. The key idea behind our approach is that we can derive the difficult-to-design forwarding and stall logic completely automatically. We have implemented a specification language for pipelined processors, along with an automatic translator that creates cycle-accurate software simulators from the specifications. We have specified a pipelined MIPS integer core in our language. The entire specification is less than 300 lines long and implements all user mode instructions except for coprocessor support. The resulting, automatically-generated, cycle-accurate simulator achieves over 240,000 instructions per second simulating MIPS machine code. This performance is within an order of magnitude of large, hand-crafted, cycle-accurate simulators, but our specification is far easier to create, read, and modify.