Rustan Leino
Biography
Rustan Leino is a Principal Researcher in the Programming Languages and Methods group at Microsoft Research, Redmond, where his research centers around programming tools. He currently leads the Spec# project, which explores enforceable contracts in object-oriented programming. He works on the design and implementation of the Spec# programming language as well as its static program verifier, called Boogie. He is also involved in a new project to verify C code, which reuses the Boogie tool.
Before joining Microsoft Research, Rustan worked as a researcher at DEC/Compaq SRC, where among other things he led the Extended Static Checking for Java (ESC/Java) project, a light-weight program checker built on the technology of program verification. His PhD thesis from Caltech (1995) addressed an important specification problem in ESC/Modula-3. Before going to graduate school, Leino worked as a software developer and technical lead in Windows/NT at Microsoft. He has written code that shipped in releases of Windows 3.0, Windows 3.1, and Windows/NT 3.5.
In his spare time, he plays and records music, teaches step aerobics, and spends time with his wife and four children.
Personal Webpage
Rustan Leino's personal webpage can be found at: http://research.microsoft.com/~leino/. Don't miss his impressive collection of puzzles!
Writings
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 |