Papers

KRML writing

[See also my talks page.]

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

Dafny

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.

Boogie

Boogie 2 (which supersedes BoogiePL) is a language for prescribing verification conditions.  Various frontends exist that translate other languages (like Spec#, C, and Dafny) 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

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#

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.

Other


Back to Rustan Leino's homepage.