Papers

KRML writing

[See also my talks page.]

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

  • New, 28 Mar 2013Developing Verified Programs with Dafny. [PDF]
    K. Rustan M. Leino.
    Tutorial notes, ICSE 2013.
  • New, 8 Mar 2013Verified Calculations. [PDF]
    K. Rustan M. Leino and Nadia Polikarpova.
    2013.
  • Revised, 29 Mar 2013Co-induction Simply. [PDF]
    K. Rustan M. Leino and Michał Moskal.
    2013.
  • Abstract Read Permissions: Fractional Permissions without the Fractions. [PDF]
    Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers.
    VMCAI 2013.
  • Automating Induction with an SMT Solver. [PDF]
    K. Rustan M. Leino.
    VMCAI 2012.
  • Tools and Behavioral Abstraction: A Direction for Software Engineering. [PDF]
    K. Rustan M. Leino.
    Future of Software Engineering symposium (FOSE), 2010
  • Stepwise Refinement of Heap-Manipulating Code in Chalice. [PDF]
    K. Rustan M. Leino and Kuat Yessenov.
    2012
  • Behavioral Interface Specification Languages.   [PDF]
    John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson
    ACM Computing Surveys, 2012.

    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.