Papers

[See also my talks page.]

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

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.

• This is Boogie 2.  [PDF]
  K. Rustan M. Leino.
  This is the working draft of the Boogie 2 language reference manual.  I expect a number of changes to this draft in the next couple of months.
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs.  [PDF]
  Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.
  FMCO 2005.
• HOL-Boogie -- an interactive prover for the Boogie program-verifier.  [PDF]
  Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff.
  To appear at TPHOLs 2008.
• A verifying compiler for a multi-threaded object-oriented language.  [PDF]
  K. Rustan M. Leino and Wolfram Schulte.
  To appear in the Marktoberdorf Summer School 2006 lecture notes.
• Weakest-Precondition of Unstructured Programs.  [PDF]
  Mike Barnett and K. Rustan M. Leino.
  PASTE 2005.
• BoogiePL: A typed procedural language for checking object-oriented programs.
  Rob DeLine and K. Rustan M. Leino.
  Technical Report MSR-TR-2005-70.
  Note:  The language BoogiePL is superseded by the language Boogie 2, whose reference manual above contains much more detail.

Dafny

Dafny is an object-based language where specifications are written in the style of dynamic frames.  Static verification of Dafny programs is done via a translation from Dafny into the Boogie language.

• Specification and verification of object-oriented software.  [PDF]
  K. Rustan M. Leino.
  Marktoberdorf International Summer School 2008, pre-lecture notes.

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

• The Spec# programming system:  Challenges and directions.  [PDF]
  Mike Barnett, Robert DeLine, Bart Jacobs, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter.
  Position paper at VSTTE 2005.
• The Spec# programming system: An overview.  [PDF]
  Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte.
  CASSIS 2004.
• Exception safety for C#.  [PDF]
  K. Rustan M. Leino and Wolfram Schulte.
  SEFM 2004.
• Declaring and checking non-null types in an object-oriented language.  [PDF]
  Manuel Fähndrich and K. Rustan M. Leino.
  OOPSLA 2003.

Specifications and methodology

• Flexible immutability with frozen objects.  [PDF]
  K. Rustan M. Leino, and Peter Müller, and Angela Wallenburg.
  To appear at VSTTE 2008.
• Verification of equivalent-results methods.  [PDF]
  K. Rustan M. Leino and Peter Müller.
  ESOP 2008.
• Class-local object invariants.  [PDF]
  K. Rustan M. Leino and Angela Wallenburg.
  ISEC 2008.
• Using history invariants to verify observers.  [PDF]
  K. Rustan M. Leino and Wolfram Schulte.
  ESOP 2007.
• Practical reasoning about invocations and implementations of pure methods.  [PDF]
  Ádám Darvas and K. Rustan M. Leino.
  FASE 2007.
• A verification methodology for model fields.  [PDF]
  K. Rustan M. Leino and Peter Müller.
  ESOP 2006.
• Safe concurrency for aggregate objects with invariants.  [PDF]
  Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte.
  SEFM 2005.
• Modular verification of static class invariants.  [PDF]
  K. Rustan M. Leino and Peter Müller.
  FM 2005.
• Object invariants in dynamic contexts.  [PDF]
  K. Rustan M. Leino and Peter Müller.
  ECOOP 2004.
• Verification of object-oriented programs with invariants.  [Electronic version]
  Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte.
  Journal of Object Technology, 2004.

Verification condition generation

• Automatic verification of textbook programs that use comprehensions.  [PDF]
  K. Rustan M. Leino and Rosemary Monahan.
  A previous version of this paper appeared at FTfJP 2007.  [PDF]

Inference techniques

• Inferring object invariants.  [PDF]
  Bor-Yuh Evan Chang and K. Rustan M. Leino.
  AIOOL 2005.

Inference and decision procedues

• Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain.  [PDF]
  K. Rustan M. Leino and Francesco Logozzo.
  WING 2007.
• Loop Invariants on Demand.  [PDF]
  K. Rustan M. Leino and Francesco Logozzo.
  APLAS 2005.
• A two-tier technique for supporting quantifiers in a lazily proof-explicating theorem prover.  [PDF]
  K. Rustan M. Leino, Madan Musuvathi, and Xinming Ou.
  TACAS 2005.
• Abstract Interpretation with Alien Expressions and Heap Structures.  [PDF]
  Bor-Yuh Evan Chang and K. Rustan M. Leino.
  VMCAI 2005.

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.

• An overview of JML tools and applications.  [PDF]
  Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll.
  STTT 7(3).  A previous version of this paper presented at FMICS 2003.
• Efficient weakest preconditions.
  K. Rustan M. Leino.
  IPL 93(6), 2005.  A previous version appeared as Technical Report MSR-TR-2004-34.
• Generating error traces from verification-condition counterexamples.  [PDF]
  K. Rustan M. Leino, Todd Millstein, and James B. Saxe.
  SCP 55(1-3), 2004.
• Extended static checking for Java.  [PDF]
  Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.
  PLDI'02.

Other

• Specification and verification challenges for sequential object-oriented programs.  [PDF]
  Gary T. Leavens, K. Rustan M. Leino, and Peter Müller.
  Formal Aspects of Computing.
• Heap monotonic typestates.  [PDF]
  Manuel Fähndrich and K. Rustan M. Leino.
  IWACO, 2003.
• A SAT characterization of boolean-program correctness.  [PDF] Copyright Springer-Verlag.
  K. Rustan M. Leino.
  SPIN 2003.
  As presented at IFIP WG 2.4 meeting, Dagstuhl: [PowerPoint]
• Finding stale-value errors in concurrent programs.  [PDF]
  Michael Burrows and K. Rustan M. Leino.
  Concurrency and Computation: Practice and Experience 16(12), 2004.
• In-place refinement for effect checking.  [PDF]
  Viktor Kuncak and K. Rustan M. Leino.
  AVIS 2003.
• Using data groups to specify and check side effects.  [PDF]
  K. Rustan M. Leino, Arnd Poetzsch-Heffter, and Yunhong Zhou.
  PLDI'02.
• Data abstraction and information hiding.  [PDF]
  K. Rustan M. Leino and Greg Nelson.
  TOPLAS 24(5), pages 491-553, ACM, September 2002.
• Data groups: Specifying the modification of extended state.  [PDF]
  K. Rustan M. Leino.
  OOPSLA '98.