Rustan Leino


Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. He is known for his work on programming languages, programming methods, and program verification, and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.

Prior to Microsoft Research, Rustan worked as a researcher at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft. He is a member (and currently Vice Chair) of IFIP Working Group 2.3, "Programming Methodology".

Rustan was first introduced to calculational methods and program correctness in a course taught by Wim Feijen at The University of Texas at Austin. Much of his research in the last 20 years has been trying to provide this rigorous thinking process into a machine checked, fluid thinking tool that can be used by a larger community of programmers. Currently, his flagship tool is the programming language and verifier Dafny. Rustan gets a lot of enjoyment from writing, in front of audiences, verifiably correct programs -- including little programs he learnt to do by hand in Wim Feijen's course. Mixing programming and proving, the Dafny language includes a "calc" statement [joint work with Nadia Polikarpova] that admits calculational proofs written in a style like that found in many places here on Dafny is used in some part of teaching at more than 25 universities.

Personal Webpage

Rustan Leino's personal webpage can be found at: Don't miss his impressive collection of puzzles!

Learn more about verification from Rustan and colleagues on his youtube channel Verification Corner. You can use Dafny in your web browser.


Below you can find a handful of Rustan's writings, about which he offers the following disclaimer:

These KRML notes have been something like my lab notebook, and as such they may contain incomplete thoughts and missing or faulty proofs. They certainly lack descriptions of all related work, may sometimes have discovered known results independently, and may in some cases be but my own interpretation of known facts or the work by others.

Number Title Other contributors
KRML23 The proof of a card trick  
KRML25 A proof in the relational calculus H. Peter Hofstee
KRML31 The rational square roots are the perfect squares Greg Nelson
KRML32 A necessary and sufficient condition for rational roots Rajit Manohar, Greg Nelson
KRML39 The specification of a consumer  
KRML41 Semaphore specifications: Larch meets Martin H. Peter Hofstee, Jan L.A. van de Snepscheut
KRML43 Specifications and private data: A call for privatizable variables  
KRML45 Data Abstraction in Multiple Scopes  
KRML46 Cardinality of sets and their powersets: Look, Ma! No case studies. Berna L. Massingill
KRML51 Pointwise dependencies in data abstraction Greg Nelson
KRML54 Beyond stacks Greg Nelson
KRML55 Modeling subtypes with only one object type  
KRML57 Specifying the state of modules David L. Detlefs
KRML58 Read-only by specification Greg Nelson
KRML59 The specification of a concurrent consumer Greg Nelson, James B. Saxe
KRML62 Object specifications: Larch meets dependencies Raymie Stata
KRML63 A myth in the modular specification of programs  
KRML65 Ecstatic: An object-oriented programming language with axiomatic semantics  
KRML73 The problem of the hidden card  
KRML74 Checking object invariants Raymie Stata
KRML76 A small dual-isomorphism lattice with no involutory dual automorphism Lyle Ramshaw
KRML81 Reachability has a last step Rajeev Joshi
KRML87 Positively capjunctive cappings, and Galois  
KRML95 The Golden Rule of Positive Integers Lyle Ramshaw