Kodkod is an efficient SAT-based analysis engine for first order logic with relations, transitive closure, and partial instances. The current prototype, which includes a finite model finder and a minimal unsatisfiable core extractor, is being used as a backend to the Karun, Forge, and Miniatur code checkers, a course scheduler, the Alloy Analyzer 4.0, a network configuration tool, etc.

We have developed a new approach to formulating and checking cryptographic protocols. It does not enable any new form of analysis. Instead, it makes verification more accessible to the designers of protocols. Its key contribution is a new characterization of these protocols that is both closer to how designers conceive them, and amenable to a direct encoding in standard first-order logic. This more direct encoding allows existing tools to be applied as black boxes without modification; it requires no tweaking of parameters or issuing of special directives by the user. Moreover, because the semantic gap between informal descriptions of protocols and their formalization is smaller, there are fewer opportunities for errors to creep in.

Type systems have been studied extensively for programming languages, but not for specification languages. We have developed a type system for the increasingly important class of specification languages based on first-order constraints over relational data models, which have applications in software modelling, architectural description, web ontologies, access control, etc.

Alloy is a software modelling language that can describe complex structures and their evolution, and which is amenable to fully automatic analysis. The Alloy Analyzer is a tool for analyzing models written in Alloy. It can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and can check user-specified properties of a model. Alloy and its analyzer have been used to find errors in several published systems, applied by several companies to internal products, and taught in a number of university courses. Alloy has also been used for generating structurally complex test cases from declarative specifications, for checking correctness of heapmanipulating Java procedures, for runtime conformance checking of object-oriented code, and for establishing the exact formal properties of an algorithm to be proved with a theorem prover.