Papers

[See also my talks page.]

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

Spec# and Boogie

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).

New papers

• Flexible immutability with frozen objects.  [PDF]
  K. Rustan M. Leino, and Peter Müller, and Angela Wallenburg.

(The new papers are also listed below.)

Specifications and methodology

• Flexible immutability with frozen objects.  [PDF]
  K. Rustan M. Leino, and Peter Müller, and Angela Wallenburg.
• 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.
• 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.
• 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.
• 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.

System and language features

• 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.
• 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.
  In CASSIS 2004 post-proceedings.
• 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.
  Appeared at OOPSLA 2003.

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]
• 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.

Inference techniques and decision procedures

• 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.
• Inferring object invariants.  [PDF]
  Bor-Yuh Evan Chang and K. Rustan M. Leino.  AIOOL 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.  To appear at 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

• Heap monotonic typestates.  [PDF]
  Manuel Fähndrich and K. Rustan M. Leino.
  Presented at 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.
  Presented at 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.