KRML writing

[See also my talks page.]

Here are some of my recent papers.  For full citations, please see my CV.


Dafny is a programming language designed with verification in mind.  It supports specifications that can be used to write functional-correctness conditions for the program.  Dafny has a static program verifier that verifies that the program meets its specifications.  The verifier is implemented on top of the Boogie verification engine.

This is the general Dafny paper:

Here are some tutorials and examples (see also the case studies below):

These papers describe technology underlying Dafny:

Here are various case studies done in Dafny.  Further examples are found in the papers above.  For a larger use of Dafny, see the "Ironclad Apps" paper at OSDI 2014 and the "Iron Fleet" papar at SOSP 2015.


Jennisys is a programming language that emphasizes specifications and data-structure invariants, rather than the code.  The idea is that straightforward code can be synthesized, so it's better from the language perspective to encourage and enable programmers to write down the essential parts of their design.  The slogan of Jennisys is "This is where programs begin".


Boogie 2 (which, since 2008, supersedes BoogiePL) is a language for prescribing verification conditions.  Various frontends exist that translate other languages (like Dafny, Eiffel, C, and Spec#) and tools (like SMACK, STORM, and GPUVerify) into Boogie.  The Boogie language can be used as a verification tool bus for various source-language frontends, program inference "mid-ends" (Boogie-to-Boogie translators), and theorem-prover based backends.  The Boogie tool verifies Boogie programs using a choice of theorem prover, the default one being the SMT solver Z3.


Chalice is an experimental language that explores the specification and verification of concurrent programs using shared memory and mutual exclusion via locks.  The semantic model for the language uses fractional permissions that can be transferred between threads and monitors.  Static verification of Chalice programs is done via a translation from Chalice into the Boogie language.


Spec# (pronounced "speck sharp") is a programming system aimed at improving the development and maintenance of correct software.  It consists of the Spec# programming language (a superset of the object-oriented .NET language C#, adding non-null types and code contracts), the Spec# compiler (which emits run-time checks to enforce the contracts), and the Boogie static program verifier (which attempts to prove a program correct with respect to its contracts).

Somewhat confusingly, the frontend that translates compiled Spec# (that is, .NET bytecode, aka MSIL) into the Boogie language has been engineered as a part of the Boogie tool that also processes Boogie programs directly.  In other words, the Spec#-to-Boogie translation and the Boogie-to-theorem-prover-input translation are both housed in the same tool, called Boogie.  Therefore, the Spec# static program verifier is known as Boogie.

More confusingly, because the static verification of Spec# programs is done by the Boogie tool, the methodology used to specify Spec# program has been called the Boogie methodology.  In retrospect, a better name would have been the Spec# methodology.

System and language features

Specifications and methodology

Verification condition generation

Inference techniques

Inference and decision procedues

ESC/Java and JML

The Java Modeling Language (JML) is a notation for writing specifications for Java programs.  An impressive array of tools have been build around JML.  One of those tools is the Extended Static Checker for Java (ESC/Java), an automatic high-precision programming tool for finding errors in Java programs.  ESC/Java works by translating JML-annotated Java programs into logical verification conditions, which are then scrutinized by an automatic theorem prover.  The checker has evolved into ESC/Java 2, which accepts the full JML language.


Back to Rustan Leino's homepage.