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 mathmeth.com. Dafny is used in some part of teaching at more than 25 universities.
Rustan Leino's personal webpage can be found at: http://research.microsoft.com/~leino/. 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 |