K. Rustan M. Leino

Rustan Leino

Senior Principal Applied Scientist, Amazon Web Services

Seattle, WA, USA

Email:  familyname at companyname .com
Home page:  https://leino.science

Research interests - Research projects - Education - Employment

Publications - Presentations

Professional distinctions - Advisory committees - Mentoring - Other professional activities - Patents

Shareware computer games - Compact discs - Videos and soundtracks - Original music - Some musical appearances - Some extracurricular activities

Research interests

My work focuses on formal verification, programming languages, and and software-correctness tools for software engineers.

Research projects

Dafny Dafny is a programming language designed with verification in mind, and its compiler includes a state-of-the-art program verifier.  The language offers forms of both imperative and functional programming and can also be used to express some mathematics.  The verifier runs in the background of the development environment.  Dafny has been used to verify challenging algorithms, is used in teaching at several universities, and has been used by award-winning teams at program verification competitions.  Dafny excels at providing an accessible integrated verification experience.
Joint work with Reza Ahmadi, Nada Amin, Chris Hawblitzel, Jason Koenig, Jay R. Lorch, Dan Matichuk, Michał Moskal, Peter Müller, Clément Pit--Claudel, Bryan Parno, Nadia Polikarpova, Tiark Rompf, Dan Rosén, Valentin Wüstholz, and others.
2008-present.
Jennisys Jennisys ("this is where programs begin") is a program synthesizer.
Joint work with Aleksandar Milicevic.
2011-2012.
Chalice Chalice is an experimental language for concurrency.  Its specifications are based on Implicit Dynamic Frames with fractional permissions.
Joint work with Stefan Heule, Peter Müller, Jan Smans, Alex J. Summers, Kuat Yessenov, and others.
2009-present.
Boogie Boogie is an Intermediate Verification Language and a verification engine for that language.  It is used by more than a dozen verifiers for different languages.
Joint work with Mike Barnett, Sascha Böhme, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, Michał Moskal, Shaz Qadeer, Philipp Rümmer, and others.
2003-present.
Spec# Spec# is a superset of the language C# 2.0, adding contracts and non-null types.  It includes a static verifier for the contracts.
Joint work with Mike Barnett, Ádám Darvas, Manuel Fähndrich, Bart Jacobs, Ronald Middelkoop, Peter Müller, Wolfram Schulte, Herman Venter, Angela Wallenburg, and others.
2003-2009.
Houdini Houdini is a specification wizard, originally for ESC/Java.  The technique infers specifications by guessing candidate specifications and then running an underlying checker to refute bad guesses.
Joint work with Cormac Flanagan, Rajeev Joshi, Michael Y. Levin, and others.
1999-2001.
ESC/Java ESC/Java (which won the Most Influential 2002 PLDI Paper award) is a formal-methods based tool for statically finding software defects in Java programs.
Joint work with Cormac Flanagan, Gary T. Leavens, Mark Lillibridge, Todd Millstein, Greg Nelson, James B. Saxe, Raymie Stata, and others.
1997-2001.
ESC/Modula-3 ESC is the original Extended Static Checker for the Modula-3 language.
Joint work with David L. Detlefs, Greg Nelson, and James B. Saxe.
1994-1996.
Modula-3D A variant of the Modula-3 language for programming multicomputers.
1992-1993.

Education

PhD Computer Science, California Institute of Technology, 1995.
Advisor:  Prof. Dr. K. Mani Chandy
MS Computer Science, California Institute of Technology, 1993.
Advisor:  Prof. Dr. Jan L. A. van de Snepscheut
BA with Special Honors in Computer Science, The University of Texas at Austin, 1989.
Honors research advisor:  Prof. Dr. Louis E. Rosier

Employment

Amazon
Seattle, WA, USA		 Senior Principal Engineer (2017-present)
Microsoft
Redmond, WA, USA		 Principal Researcher (2007-2017)
Senior Researcher (2006-2007)
Researcher (2001-2006)
Software design engineer, technical lead (1989-1991)
Imperial College London
London, UK		 Visiting Professor (honorary post, 2012-2017)
DEC/Compaq
Systems Research Center
Palo Alto, CA, USA		 Computer science researcher (Jan 1995-Nov 2001)
Research intern (summer 1994)
Research intern (summer 1992)
Caltech
Pasadena, CA, USA		 Co-instructor, Mathematics of Program Construction (Fall 1994)
Co-instructor, Mathematics of Program Construction (Spring 1994)
Teaching assistant, Computation, Computers, Programs (Fall 1991-Spring 1994)
Graduate research assistant (Fall 1991-Fall 1994)
CompuGuide
Austin, TX, USA		 President, consultant (Feb 1988-May 1989)
UT Austin
Informal Classes
Austin, TX, USA		 Instructor of various computer classes (Sep 1987-May 1989)
One-Eleven, Inc.
Austin, TX, USA		 Programmer (Aug 1987-May 1989)

Publications

(Caution: Contents has not been updated since January 2017.)

   Legend
B Books, Chapters, Lecture Notes
V Edited Volumes
J Journal Articles
C In Conference Proceedings
Th Theses
O Other
 
O Quicksort Revisited—Verifying Alternative Versions of Quicksort TPFM 2016
Razvan Certezeanu, Sophia Drossopoulou, Benjamin Egelund-Muller, K. Rustan M. Leino, Sinduran Sivarajan, and Mark Wheelhouse
In Erika Ábrahám, Marcello M. Bonsangue, and Einar Broch Johnsen, editors, Theory and Practice of Formal Methods—Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 407-426.  Springer, 2016.
C Trigger Selection Strategies to Stabilize Program Verifiers CAV 2016
K. Rustan M. Leino and Clément Pit-Claudel
In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification—28th International Conference, CAV 2016, volume 9779 of Lecture Notes in Computer Science, pages 361-381.  Springer, July 2016.
C Integrated Environment for Diagnosing Verification Errors TACAS 2016
Maria Christakis, K. Rustan M. Leino, Peter Müller, and Valentin Wüstholz
In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems—22nd International Conference, TACAS 2016, volume 9636 of Lecture Notes in Computer Science, pages 424-441.  Springer, April 2016.
V Verification, Model Checking, and Abstract Interpretation—17th International Conference, VMCAI 2016 LNCS
(VMCAI 2016)
Barbara Jobstmann and K. Rustan M. Leino
Volume 9583 of Lecture Notes in Computer Science.  Springer, January 2016.
J An Assertional Proof of the Stability and Correctness of Natural Mergesort ACM Comp. Logic
K. Rustan M. Leino and Paqui Lucio
ACM Transactions on Computational Logic, 17(1): 6, December 2015.
C Fine-Grained Caching of Verification Results CAV 2015
K. Rustan M. Leino and Valentin Wüstholz
In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification—27th International Conference, CAV 2015, Proceedings, Part I, volume 9206 of Lecture Notes in Computer Science, pages 380-397.  Springer, July 2015.
O Automatic verification of Dafny programs with traits FTfJP@ECOOP 2015
Reza Ahmadi, K. Rustan M. Leino, and Jyrki Nummenmaa
In Rosemary Monahan, editor, Proceedings of the 17th Workshop on Formal Techniques for Java-like Programs, FTfJP 2015, pages 4:1-4:5.  ACM, 2015.
O Well-founded Functions and Extreme Predicates in Dafny: A Tutorial IWIL-2015
K. Rustan M. Leino
In Boris Konev, Stephan Schulz, and Laurent Simon, editors, IWIL-2015. 11th International Workshop on the Implementation of Logics, volume 40 of EPiC Series in Computing, pages 106-118.  EasyChair, 2016.
O Compiling Hilbert's epsilon operator LPAR short papers 2015
K. Rustan M. Leino
In Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, editors, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning—Short Presentations, LPAR 2015, volume 35 of EPiC Series in Computing, pages 106-118.  EasyChair, 2015.
O Programming Language Features for Refinement Refine@FM 2015
Jason Koenig and K. Rustan M. Leino
In John Derrick, Eerke A. Boiten, and Steve Reeves, editors, Proceedings 17th International Workshop on Refinement, Refine@FM 2015, volume 209 of Electronic Proceedings in Theoretical Computer Science, pages 87-106.  2016.
C Co-induction simply—Automatic Co-inductive Proofs in a Program Verifier FM 2014
K. Rustan M. Leino and Michał Moskal
In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: 19th International Symposium on Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 382-398.  Springer, May 2014.
C Formalizing and Verifying a Modern Build Language FM 2014
Maria Christakis, K. Rustan M. Leino, and Wolfram Schulte
In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: 19th International Symposium on Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 643-657.  Springer, May 2014.
C Computing with an SMT Solver TAP 2014
Nada Amin, K. Rustan M. Leino, and Tiark Rompf
In Martina Seidl and Nikolai Tillmann, editors, Tests and Proofs—8th International Conference, TAP 2014, volume 8570 of Lecture Notes in Computer Science, pages 20-35.  Springer, July 2014.
O The Dafny Integrated Development Environment F-IDE 2014
K. Rustan M. Leino and Valentin Wüstholz
In Catherine Dubois, Dimitra Giannakopoulou, and Dominique Méry, editors, 1st Workshop on Formal-IDE, volume 149 of Electronic Proceedings in Theoretical Computer Science.  April 2014.
C Automating Theorem Proving with SMT ITP 2013
K. Rustan M. Leino
In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, 4th International Conference, ITP 2013, volume 7998 of Lecture Notes in Computer Science, pages 2-16.  Springer, July 2013.
C Developing Verified Programs with Dafny ICSE 2013
K. Rustan M. Leino
In David Notkin, Betty H. C. Cheng, and Klaus Pohl, editors, 35th International Conference on Software Engineering, ICSE '13, pages 1488-1490.  ACM, May 2013.
C Verified Calculations VSTTE 2013
K. Rustan M. Leino and Nadia Polikarpova
In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments—5th International Conference, VSTTE 2013, Revised Selected Papers, volume 8164 of Lecture Notes in Computer Science, pages 170-190.  Springer, 2014.
O Co-induction Simply:  Automatic Co-inductive Proofs in a Program Verifier MSR TR
K. Rustan M. Leino and Michal Moskal
Technical Report MSR-TR-2013-49, Microsoft Research, May 2013.
V Tools for Software Verification:  special section from the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems STTT
(from TACAS 2011)
Parosh Aziz Abdulla and K. Rustan M. Leino
Software Tools for Technology Transfer, 15(2).  April 2013.
C Abstract Read Permissions: Fractional Permissions without the Fractions VMCAI 2013
Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers
In Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni, editors, Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, volume 7737 of Lecture Notes in Computer Science, pages 315-334.  Springer, January 2013.
B Using Dafny, an Automatic Program Verifier LASER 2011
Luke Herbert, K. Rustan M. Leino, and Jose Quaresma
In Bertrand Meyer and Martin Nordio, editors, Tools for Practical Software Verification, {LASER}, International Summer School 2011, volume 7682 of Lecture Notes in Computer Science, pages 156-181.  Springer, 2012.
C Program extrapolation with Jennisys OOPSLA 2012
K. Rustan M. Leino and Alexandar Milicevic
In Gary T. Leavens and Matthew B. Dwyer, editors, Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012, pages 411-430.  ACM, October 2012.
J Stepwise refinement of heap-manipulating code in Chalice FAC
K. Rustan M. Leino and Kuat Yessenov
Formal Aspects of Computing, 24(4-6): 519-535, July 2012.
Celebrating the 60th Birthday of Carroll Morgan.
O Endorsement blurb  
K. Rustan M. Leino
On back cover of SPARK - The Proven Approach to High Integrity Software.  John Barnes with Altran Praxis.  Altran Praxis, 2012.
O The EventB2Dafny Rodin plug-in TOPI 2012
Néstor Cataño, K. Rustan M. Leino, and Victor Rivera
In 2nd Workshop on Developing Tools as Plug-ins (TOPI), pages 49-54.  IEEE, June 2012.
J Behavioral Interface Specification Languages Comp. Surv.
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson
ACM Computing Surveys, 44(3): 16, June 2012.
V Special issue:  Selected Papers of the Confrence 'Tools and Algorithms for the Construction and Analysis of Systems "TACAS" 2011' LMCS
(from TACAS 2011)
Parosh Aziz Abdulla and K. Rustan M. Leino
Logical Methods in Computer Science.  DOI: 10.2168/LMCS-TACAS:2011.  2012.
http://www.lmcs-online.org/ojs/specialIssues.php?id=40
B Getting Started with Dafny: A Guide MOD 2011
Jason Koenig and K. Rustan M. Leino
In Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann, editors, Software Safety and Security: Tools for Analysis and Verification.  NATO Science for Peace and Security Series D: Information and Communication Security.  IOS Press, 2012, volume 33, pages 152-181.
Marktoberdorf International Summer School 2011 lecture notes.
C Automating Induction with an SMT Solver VMCAI 2012
K. Rustan M. Leino
In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, volume 7148 of Lecture Notes in Computer Science, pages 315-331.  Springer, January 2012.
C The Boogie Verification Debugger (Tool Paper) SEFM 2011
Claire Le Goues, K. Rustan M. Leino, and Michał Moskal
In Gilles Barthe, Alberto Pardo, and Gerardo Schneider, editors, Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pages 407-414.  Springer, November 2011.
C The 1st Verified Software Competition: Experience Report FM 2011
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiβ
In Michael Butler and Wolfram Schulte, editors, FM 2011: Formal Methods - 17th International Symposium on Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 154-168.  Springer, June 2011.
FM 2011 Best Paper Award.
J Specification and verification: the Spec# experience CACM
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte, and Herman Venter
Communications of the ACM, 54(6): 81-91, June 2011.
V Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011 LNCS
(TACAS 2011)
Parosh Aziz Abdulla and K. Rustan M. Leino
Volume 6605 of Lecture Notes in Computer Science.  Springer, March-April 2011.
J Doomed program points FMSD
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies
Formal Methods in System Design, 37(2-3): 171-199, December 2010.
B Tools and Behavioral Abstraction: A Direction for Software Engineering FOSE 2010
K. Rustan M. Leino
In Sebastian Nanz, editor, The Future of Software Engineering, pages 115-124.  Springer, November 2010.
Festschrift for Bertrand Meyer on the Occasion of His 60th Birthday.
O Usable Auto-Active Verification UV 2010
K. Rustan M. Leino and Michał Moskal
In Tom Ball, Lenore Zuck, and N. Shankar, editors, UV10 (Usable Verification) workshop.  November 2010.  http://fm.csl.sri.com/UV10/
O VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0 VSTTE 2010 workshop
K. Rustan M. Leino and Michał Moskal
In Tools and Experiments workshop at VSTTE 2010.  August 2010. 
C Dafny Meets the Verification Benchmarks Challenge VSTTE 2010
K. Rustan M. Leino and Rosemary Monahan
In Gary T. Leavens, Peter W. O'Hearn, and Sriram K. Rajamani, editors, Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, volume 6217 of Lecture Notes in Computer Science, pages 112-126.  Springer, August 2010.
C To Goto Where No Statement Has Gone Before VSTTE 2010
Mike Barnett and K. Rustan M. Leino
In Gary T. Leavens, Peter W. O'Hearn, and Sriram K. Rajamani, editors, Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, volume 6217 of Lecture Notes in Computer Science, pages 157-168.  Springer, August 2010.
J Learning to do program verification CACM
K. Rustan M. Leino
Communications of the ACM, 53(6): 106, June 2010.
Technical Perspective, introducing the article seL4: Formal Verification of an Operating-System Kernel by Gerwin Klein et al.
C Dafny: An Automatic Program Verifier for Functional Correctness LPAR-16
K. Rustan M. Leino
In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, volume 6355 of Lecture Notes in Computer Science, pages 348-370.  Springer, April-May 2010.
C Deadlock-Free Channels and Locks ESOP 2010
K. Rustan M. Leino, Peter Müller, and Jan Smans
In Andrew D. Gordon, editor, Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, volume 6012 of Lecture Notes in Computer Science, pages 407-426.  Springer, March 2010.
C A Polymorphic Intermediate Verification Language: Design and Logical Encoding TACAS 2010
K. Rustan M. Leino and Philipp Rümmer
In Javier Esparza and Rupak Majumdar, editors, Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, volume 6015 of Lecture Notes in Computer Science, pages 312-327.  Springer, March 2010.
B Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs LASER 2007/2008
K. Rustan M. Leino and Peter Müller
In Peter Müller, editor, Advanced Lectures on Software Engineering, LASER Summer School 2007/2008, volume 6029 of Lecture Notes in Computer Science, pages 91-139.  Springer, 2010.
C It's Doomed; We Can Prove It FM 2009
Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies
In Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, Second World Congress, volume 5850 of Lecture Notes in Computer Science, pages 338-353.  Springer, November 2009.
C A Basis for Verifying Multi-threaded Programs ESOP 2009
K. Rustan M. Leino and Peter Müller
In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on programming, ESOP 2009, pages 378-393.  Springer, March 2009.
C Proving Consistency of Pure Methods and Model Fields FASE 2009
K. Rustan M. Leino and Ronald Middelkoop
In Marsha Chechik and Martin Wirsing, editors, Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, pages 231-245.  Springer, March 2009.
B Verification of Concurrent Programs with Chalice  
K. Rustan M. Leino, Peter Müller, and Jan Smans
In Alessandro Aldini, Gilles Barthe, Roberto Gorrieri, editors, Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 195-222.  Springer, 2009.
C Reasoning about Comprehensions with First-Order SMT Solvers SAC 2009
K. Rustan M. Leino and Rosemary Monahan
In 2009 Symposium on Applied Computing, pages 615-622.  ACM, March 2009.
A previous version of this article had the title Automatic verification of textbook programs that use comprehensions.
B Specification and verification of object-oriented software MOD 2008
K. Rustan M. Leino
In Manfred Broy, Wassiou Sitou, and Tony Hoare, editors, Engineering Methods and Tools for Software Safety and Security.  NATO Science for Peace and Security Series D: Information and Communication Security.  IOS Press, 2009, volume 22, pages 231-266.
Marktoberdorf International Summer School 2008 lecture notes.
J A programming model for concurrent object-oriented programs TOPLAS
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, Wolfram Schulte, and Jan Smans
ACM Transactions on Programming Languages and Systems, 31(1), December 2008.
C Flexible immutability with frozen objects VSTTE 2008
K. Rustan M. Leino, Peter Müller, and Angela Wallenburg
In Jim Woodcock and N. Shankar, editors, Verified Software: Theories, Tools, Experiments, VSTTE 2008, volume 5295 of Lecture Notes in Computer Science, pages 192-208.  Springer, October 2008.
O Verification Condition Splitting MSR TR
K. Rustan M. Leino, Michał Moskal, and Wolfram Schulte
Technical Report, Microsoft Research, October 2008.
C HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier TPHOLs 2008
Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff
In Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, volume 5170 of Lecture Notes in Computer Science, pages 150-166.  Springer, August 2008.
C Position Statement: Ceaselessly-Analyzing Development Environments, One Direction for the Next 40 Years of Software Engineering COMPAC 2008
K. Rustan M. Leino
In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference, COMPSAC 2008, page 11.  IEEE Computer Society, August 2008.
O This is Boogie 2 MSR TR
K. Rustan M. Leino
Technical Report, Microsoft Research, June 2008.
C Verification of equivalent-results methods ESOP 2008
K. Rustan M. Leino and Peter Müller
In Sophia Drossopoulou, editor, Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, volume 4960 of Lecture Notes in Computer Science, pages 307-321.  Springer, March/April 2008.
C Class-local object invariants ISEC 2008
K. Rustan M. Leino and Angela Wallenburg
In Proceedings of the 2008 First India Software Engineering Conference, pages 57-66.  ACM, February 2008.
O Using widenings to infer loop invariants inside an SMT solver, or: A theorem prover as abstract domain WING 2007
K. Rustan M. Leino and Francesco Logozzo
In proceedings of Workshop on Invariant Generation (WING 2007), June 2007.
J Specification and verification challenges for sequential object-oriented programs FAC
Gary T. Leavens, K. Rustan M. Leino, and Peter Müller
Formal Aspects of Computing, 19(2):159-189, June 2007.
C Using history invariants to verify observers ESOP 2007
K. Rustan M. Leino and Wolfram Schulte
In Rocco De Nicola, editor, Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, volume 4421 of Lecture Notes in Computer Science, pages 80-94.  Springer, March 2007.
C Practical reasoning about invocations and implementations of pure methods FASE 2007
Ádám Darvas and K. Rustan M. Leino
In Matthew B. Dwyer and Antónia Lopes, editors, Fundamental Approaches to Software Engineering, 10th International Conference, FASE 2007, volume 4422 of Lecture Notes in Computer Science, pages 336-351.  Springer, March 2007.
B A verifying compiler for a multi-threaded object-oriented language MOD 2006
K. Rustan M. Leino and Wolfram Schulte
In Manfred Broy, Johannes Grünbauer, and Tony Hoare, editors, Software Safety and Security.  NATO Science for Peace and Security Series D: Information and Communication Security.  IOS Press, 2007, volume 9, pages 351-416.
Marktoberdorf International Summer School 2006 lecture notes.
B Foreword  
K. Rustan M. Leino
Verification of Object-Oriented Software: The KeY Approach.  Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt, editors.  Volume 4334 of Lecture Notes in Artificial Intelligence, pages VII-VIII.  Springer, 2007.
C Boogie: A Modular Reusable Verifier for Object-Oriented Programs FMCO 2005
Mike Barnett, Robert DeLine, Bart Jacobs, Bor-Yuh Evan Chang, and K. Rustan M. Leino
In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects:  4th International Symposium, FMCO 2005, volume 4111 of Lecture Notes in Computer Science, pages 364-387.  Springer, September 2006.
V Verified Software: Theories, Tools, and Experiments, VSTTE 2006, Workshop proceedings MSR TR
(VSTTE 2006)
K. Rustan M. Leino and Wolfram Schulte, editors
Technical Report MSR-TR-2006-117, Microsoft Research, August 2006.
C A verification methodology for model fields ESOP 2006
K. Rustan M. Leino and Peter Müller
In Peter Sestoft, editor, Programming Languages and Systems: 15th European Symposium on Programming, ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 115-130.  Springer, March 2006.
C Loop invariants on demand APLAS 2005
K. Rustan M. Leino and Francesco Logozzo
In Kwangkeun Yi, editor, Programming Languages and Systems, Third Asian Symposium, APLAS 2005, volume 3780 of Lecture Notes in Computer Science, pages 119-134.  Springer, November 2005.
O The Spec# programming system: Challenges and directions VSTTE 2005
Mike Barnett, Robert DeLine, Bart Jacobs, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte, and Herman Venter
Position paper, Verified Software: Theories, Tools, Experiments (VSTTE 2005), October 2005.
O Weakest-precondition of unstructured programs PASTE 2005
Mike Barnett and K. Rustan M. Leino
In Michael D. Ernst and Thomas P. Jensen, editors, Proceedings of the 2005 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE'05, pages 82-87.  ACM, September 2005.
C Safe Concurrency for Aggregate Objects with Invariants SEFM 2005
Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte
In Bernhard K. Aichernig and Bernhard Beckert, editors, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pages137-146.  IEEE Computer Society, September 2005.
C Modular verification of static class invariants FM 2005
K. Rustan M. Leino and Peter Müller
In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, FM 2005: Formal Methods, International Symposium of Formal Methods Europe, volume 3582 of Lecture Notes in Computer Science, pages 26-42.  Springer, July 2005.
O BoogiePL: A typed procedural language for checking object-oriented programs MSR TR
Robert DeLine and K. Rustan M. Leino
Technical Report MSR-TR-2005-70, Microsoft Research, May 2005.
C A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover TACAS 2005
K. Rustan M. Leino, Madan Musuvathi, and Xinming Ou
In Nicolas Halbwachs and Lenore D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Software, 11th International Conference, TACAS 2005, volume 3440 of Lecture Notes in Computer Science, pages 334-348.  Springer, April 2005.
J Efficient weakest preconditions IPL
K. Rustan M. Leino
Information Processing Letters, 93(6):281-288, March 2005.
J An overview of JML tools and applications STTT
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll
International Journal on Software Tools for Technology Transfer, 7(3):212-232, 2005.
J Generating error traces from verification-condition counterexamples SCP
K. Rustan M. Leino, Todd Millstein, and James B. Saxe
Science of Computer Programming, 55(1-3):209-226, 2005.
O Inferring object invariants AIOOL 2005
Bor-Yuh Evan Chang and K. Rustan M. Leino
First international workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL), January 2005.
C Abstract interpretation with alien expressions and heap structures VMCAI 2005
Bor-Yuh Evan Chang and K. Rustan M. Leino
In Radhia Cousot, editor, Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, volume 3385 of Lecture Notes in Computer Science, pages 147-163.  Springer, January 2005.
J Finding stale-value errors in concurrent programs C&C: P&E
Michael Burrows and K. Rustan M. Leino
Concurrency and Computation: Practice and Experience, 16(12):1161-1172, October 2004.
O Modular verification of global module invariants in object-oriented programs ETHZ TR
K. Rustan M. Leino and Peter Müller
Technical Report 459, ETH Zurich, Department of Computer Science, September 2004.
C Exception safety for C# SEFM 2004
K. Rustan M. Leino and Wolfram Schulte
In Jorge R. Cuellar and Zhiming Liu, editors, SEFM 2004—Second International Conference on Software Engineering and Formal Methods, pages 218-227.  IEEE, September 2004.
C Object invariants in dynamic contexts ECOOP 2004
K. Rustan M. Leino and Peter Müller
In Martin Odersky, editor, ECOOP 2004—Object-oriented programming, 18th European Conference, Proceedings, volume 3086 of Lecture Notes in Computer Science, pages 491-516.  Springer, June 2004.
J Verification of object-oriented programs with invariants JOT
Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, and Wolfram Schulte
Journal of Object Technology, 3(6):27-56, June 2004.
O The Spec# Programming System: An overview CASSIS 2004
Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte
In Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, volume 3362 of Lecture Notes in Computer Science, pages 49-69.  Springer, March 2004.
O On computing the fixpoint of a set of boolean equations MSR TR
Viktor Kuncak and K. Rustan M. Leino
Technical Report MSR-TR-2003-08, Microsoft Research, December 2003.
Also available as cs.PL/0408045, The Computing Research Repository (CoRR).
O Declaring and checking non-null types in an object-oriented language OOPSLA 2003
Manuel Fähndrich and K. Rustan M. Leino
In Proceedings of the 2003 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'03), volume 38(11) of SIGPLAN Notices, pages 302-312.  ACM, November 2003.
B Abstraction dependencies  
K. Rustan M. Leino and Greg Nelson
In Annabelle McIver and Carroll Morgan, editors, Programming Methodology, Monographs in Computer Science, chapter 13, pages 269-289.  Springer, 2003.
O Heap monotonic typestates IWACO 2003
Manuel Fähndrich and K. Rustan M. Leino
In Proceedings of International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), July 2003.
O A SAT characterization of boolean-program correctness SPIN 2003
K. Rustan M. Leino
In Thomas Ball and Sriram K. Rajamani, editors, Model Checking Software, volume 2648 of Lecture Notes in Computer Science, pages 104-120.  Springer, May 2003.
O In-place refinement for effect checking AVIS'03
Viktor Kuncak and K. Rustan M. Leino
Presented at Second International Workshop on Automated Verification of Infinite-State Systems (AVIS'03), Warsaw, Poland, April 2003.
B A logic of object-oriented programs  
Martín Abadi and K. Rustan M. Leino
In Nachum Dershowitz, editor, Verification: Theory and Practice, Essays dedicated to Zohar Manna on the occasion of his 64th birthday, volume 2772 of Lecture Notes in Computer Science, pages 11-41.  Springer, 2003.
J Data abstraction and information hiding TOPLAS
K. Rustan M. Leino and Greg Nelson
ACM Transactions on Programming Languages and Systems, 24(5):491-553, September 2002.
C Using data groups to specify and check side effects PLDI 2002
K. Rustan M. Leino, Arnd Poetzsch-Heffter, and Yunhong Zhou
In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 37(5) of SIGPLAN Notices, pages 246-257.  ACM, May 2002.
C Extended static checking for Java PLDI 2002
Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata
In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 37(5) of SIGPLAN Notices, pages 234-245.  ACM, May 2002.
Most Influential PLDI 2012 Paper Award (awarded in 2012).
C Applications of extended static checking SAS'01
K. Rustan M. Leino
In Patrick Cousot, editor, Static Analysis: 8th International Symposium (SAS'01), volume 2126 of Lecture Notes in Computer Science, pages 185-193. Springer, July 2001.
C Houdini, an annotation assistant for ESC/Java FME 2001
Cormac Flanagan and K. Rustan M. Leino
In International Symposium of Formal Methods Europe 2001: Formal Methods for Increasing Software Productivity, volume 2021 of Lecture Notes in Computer Science, pages 500-517. Springer, March 2001.
J Annotation inference for modular checkers IPL
Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino
Information Processing Letters, 77(2-4):97-108, February 2001.
J Real estate of names IPL
K. Rustan M. Leino
Information Processing Letters, 77(2-4):169-171, February 2001.
C Extended static checking: A ten-year perspective Dagstuhl 10th anniversary
K. Rustan M. Leino
In Reinhard Wilhelm, editor, Informatics—10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 157-175. Springer, January 2001.
O ESC/Java quick reference SRC TN
Silvija Seres with K. Rustan M. Leino and James B. Saxe
Technical Note 2000-004, Compaq Systems Research Center, Palo Alto, CA, October 2000.
O ESC/Java user's manual SRC TN
K. Rustan M. Leino, Greg Nelson, and James B. Saxe
Technical Note 2000-002, Compaq Systems Research Center, Palo Alto, CA, October 2000.
O JML: Notations and tools supporting detailed design in Java OOPSLA'00 poster
Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs
In OOPSLA'00 Companion. ACM, 2000. Also available as Technical Report TR #00-15, Department of Computer Science, Iowa State University, August 2000.
J A semantic approach to secure information flow SCP
Rajeev Joshi and K. Rustan M. Leino
Science of Computer Programming, 37(1-3):113-138, May 2000.
O Checking Java programs via guarded commands FTfJP 1999
K. Rustan M. Leino, James B. Saxe, and Raymie Stata
Technical Note 1999-002, Compaq Systems Research Center, Palo Alto, CA, May 1999. Also appeared in Formal Techniques for Java Programs, workshop proceedings. Bart Jacobs, Gary T. Leavens, Peter Muller, and Arnd Poetzsch-Heffter, editors. Technical Report 251, Fernuniversität Hagen, 1999.
J Virginity: A contribution to the specification of object-oriented software IPL
K. Rustan M. Leino and Raymie Stata
Information Processing Letters, 70(2):99-105, April 1999.
J Joining specification statements TCS
K. Rustan M. Leino and Rajit Manohar
Theoretical Computer Science, 216(1-2):375-394, March 1999.
J Computing permutation encodings FAC
K. Rustan M. Leino
Formal Aspects of Computing, 11(1):56-74, 1999.
O Extended static checking SRC RR
David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe
Research Report 159, Compaq Systems Research Center, Palo Alto, CA, December 1998.
C Data groups: Specifying the modification of extended state OOPSLA '98
K. Rustan M. Leino
In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA '98), volume 33(10) of ACM SIGPLAN Notices, pages 144-153.  ACM, October 1998.
J Recursive object types in a logic of object-oriented programs NJC
K. Rustan M. Leino
Nordic Journal of Computing, 5(4):330-360, 1998.
O Wrestling with rep exposure SRC RR
David L. Detlefs, K. Rustan M. Leino, and Greg Nelson
Research Report 156, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, July 1998.
C A semantic approach to secure information flow MPC '98
K. Rustan M. Leino and Rajeev Joshi
In Johan Jeuring, editor, Mathematics of Program Construction: 4th International Conference, MPC'98, volume 1422 of Lecture Notes in Computer Science, pages 254-271. Springer, June 1998.
C Recursive object types in a logic of object-oriented programs ESOP '98
K. Rustan M. Leino
In Chris Hankin, editor, Programming Languages and Systems: 7th European Symposium on Programming, ESOP'98, volume 1381 of Lecture Notes in Computer Science, pages 170-184. Springer, April 1998.
O Tool Demonstration:  An extended static checker for Modula-3 CC'98 tool demo
K. Rustan M. Leino and Greg Nelson
In Kai Koskimies, editor, Compiler Construction: 7th International Conference, CC'98, volume 1383 of Lecture Notes in Computer Science, pages 302-305. Springer, April 1998.
O A small dual-automorphic lattice with no involutory dual automorphism SRC TN
K. Rustan M. Leino and Lyle Ramshaw
Technical Note 1997-008, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, May 1997.
C A logic of object-oriented programs TAPSOFT '97
Martín Abadi and K. Rustan M. Leino
In Michel Bidoit and Max Dauchet, editors, Theory and Practice of Software Development: Proceedings / TAPSOFT '97, 7th International Joint Conference CAAP/FASE, volume 1214 of Lecture Notes in Computer Science, pages 682-696. Springer, April 1997.
O Checking object invariants SRC TN
K. Rustan M. Leino and Raymie Stata
Technical Note 1997-007, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, January 1997.
O Ecstatic: An object-oriented programming language with an axiomatic semantics FOOL 4
K. Rustan M. Leino
In Proceedings of the Fourth International Workshop on Foundations of Object-Oriented Languages, January 1997.
J Conditional composition FAC
Rajit Manohar and K. Rustan M. Leino
Formal Aspects of Computing, 7(6):683-703, March 1995.
J Constructing a program with exceptions IPL
K. Rustan M. Leino
Information Processing Letters, 53(3):159-163, February 1995.
Th Toward reliable modular programs PhD thesis
K. Rustan M. Leino
PhD thesis, California Institute of Technology, January 1995.  Available as Technical Report Caltech CS-TR-95-03.
J A method for showing progress FAC
K. Rustan M. Leino
Formal Aspects of Computing, 7(5):567-580, January 1995.
C Semantics of exceptions PROCOMET '94
K. Rustan M. Leino and Jan L. A. van de Snepscheut
In E.-R. Olderog, editor, Programming concepts, methods, and calculi (PROCOMET'94), volume A-56 of IFIP Transactions, pages 447-466. North-Holland, June 1994.
Th Multicomputer programming with Modula-3D MS thesis
K. Rustan M. Leino
MS thesis, California Institute of Technology, June 1993.  Available as Technical Report Caltech CS-TR-93-15.
O Extensions to an object-oriented programming language for programming fine-grain multicomputers Caltech CS TR
K. Rustan M. Leino
Technical Report Caltech-CS-TR-92-26, 1992.
Th K pinwheel schedulable numbers always have 3 friends, but need not have more
K. Rustan M. Leino
Undergraduate honors research, The University of Texas at Austin, May 1989.  Unpublished manuscript.

Presentations

(other than conference and workshop presentations of papers above)

  • Automation and Dafny
    • New Directions In Software Technology (NDIST'16), St John, VI, USA (December 2016).
  • Well-founded functions, induction, and extreme predicates in an SMT-based verifier
    • Seminar, Microsoft Research, Cambridge, UK (December 2016).
  • Verification beyond programs
    • Invited talk, Workshop on Software Correctness and Reliability, Zurich, Switzerland (October 2016).
  • Certified intermediate verification language
    • IFIP WG 2.3 meeting 58, Villebrumier, France (October 2016).
  • Advanced Encodings into an Intermediate Verification Language
    • Invited talk, AutoProof workshop, Villebrumier, France (October 2016).
  • Global snapshots
    • Dr. TLA+ series lecture, Microsoft Research (and youtube), Redmond, WA, USA (September 2016).
  • Two-state lemmas
    • Lightening talk, UW PLSE Retreat 2016, Leavenworth, WA, USA (September 2016).
  • Dafny Autumn School
    • 2-day seminar, with Gudmund Grov, Edinburgh, Scotland, UK (September 2016).
  • Verification for the rest of us
    • Invited talk, MisraFest, Austin, TX, USA (April 2016).
  • Dafny tutorial
    • Invited tutorial, VerifyThis @ ETAPS 2016, Eindhoven, The Netherlands (April 2016).
  • Automated verification of functional programs
    • Dagstuhl seminar on Verification of Functional Languages, Dagstuhl, Germany (March 2016).
  • Modeling program semantics in an automated program verifier
    • Pacific Northwest PLSE 2016, Seattle, WA (March 2016).
  • Extreme predicates beyond continuity
    • IFIP WG 2.3 meeting 57, Pasadena, CA, USA (January 2016).
  • Software correctness: A personal journey
    • Invited talk, PAUSE, Villebrumier, France (December 2015).
  • The Dafny perspective on reasoning
    • Seminar, TU Darmstadt, Germany (March 2016)
    • CS Colloquium, Yale University, New Haven, CT, USA (November 2015).
  • Dafny: Programs and proofs
    • PLCLUB seminar, University of Pennsylvania, Philadelphia, PA, USA (October 2015).
  • Traits and dynamic frames
    • Semantics and Verification of Object-Oriented Languages, NII Shonan Meeting Seminar 063, Japan (September 2015).
  • Program semantics and machine-assisted proofs
    • 3-day mini-course, Imperial College London, London, UK (May 2015).
  • Programming with and implementing Hilbert's ε operator
    • IFIP WG 2.3 meeting 56, Istanbul, Turkey (March 2015).
  • Induction, Synthesis, Inference
    • Invited talk, Induction workshop, Chalmers, Göteborg, Sweden (March 2015).
  • Making program verification work
    • Seminar, U. Bergen, Norway (June 2015).
    • Seminar, CEA LIST, Paris, France (March 2015).
    • PL Seminar, UC Berkeley, CA, USA (February 2015).
  • Higher-order functions in the verification-aware programming language Dafny
    • Seminar, Imperial College London, UK (January 2015).
  • Using Dafny for proofs
    • Guest presentation, C141, Imperial College London, UK (January 2015).
  • Early Verification
    • Keynote, VMCAI 2015, joint TIFR Colloquium, Mumbai, India (January 2015).
  • Preserving intent
    • New Directions In Software Technology (NDIST'14), St John, VI, USA (December 2014).
  • Thinking for a living
    • Invited talk, Renton Rotary, Renton, WA, USA (December 2014).
  • Program verification via an intermediate verification language
    • Guest lecture in Emina Torlak's CSE 507, Computer-Aided Reasoning for Software, University of Washington, Seattle, WA (May 2016).
    • Guest lecture in Emina Torlak's CSE 507, Computer-Aided Reasoning for Software, University of Washington, Seattle, WA (October 2014).
  • An interface to symbolic methods
    • Keynote, International Workshop on Algebraic Development Techniques (WADT 2014), Sinaia, Romania (September 2014)
  • Predicates that do more
    • IFIP WG 2.3 meeting 55, Orlando, FL, USA (May 2014).
  • Using Dafny for programs and proofs
    • Invited Tutorial, AI4FM workshop, Singapore (May 2014).
  • Verifying coroutines
    • Seminar, ETH Zurich, Switzerland (April 2014).
  • Dafny crash course
    • Tutorial, Dagstuhl seminar on Evaluating Software Verification Systems: Benchmarks and Competitions, Schloss Dagstuhl, Germany (April 2014).
  • Programming in Stages
    • Invited Talk, Third workshop on Validation Strategies for Software Evolution, Grenoble, France (April 2014).
  • Theorem Proving and Program Verification with Dafny
    • 3-day mini-course, Imperial College London, London, UK (March 2014).
  • Dafny induction demo
    • Induction workshop, Imperial College London, London, UK (November 2013).
  • Theorem proving using SMT
    • Keynote, ITP 2013, Rennes, France (July 2013).
  • More co-induction
    • IFIP WG 2.3 meeting 54, Saint Petersburg, Russia (June 2013).
  • Dafny: A programming system for functional correctness
    • CS Colloquium, UCLA, Los Angeles, CA (January 2014).
    • Northrop Grumman, Carson, CA (June 2013).
    • Microsoft Development Center Copenhagen, Copenhagen, Denmark (June 2013).
    • Oracle Labs, Redwood Shores, CA (May 2013).
  • For programs and proofs:  mo' specs and mo' math
    • JML seminar, Shonan Village, Japan (May 2013).
  • Verifying coroutines
    • Imperial College, London, UK (March 2013).
  • Program Proving using Intermediate Verification Languages (IVLs) like Boogie and Why3
    • Invited plenary talk, HILT 2012, Boston, MA (December 2012).
  • Developing verified programs with Dafny
    • Tutorial, SPLASH 2013, Indianapolis, IN (October 2013).
    • Tutorial, ICSE 2013, San Francisco, CA (May 2013).
    • Tutorial, HILT 2012, Boston, MA (December 2012).
  • Dafny and other tools in RiSE
    • NASA Ames, Moffett Field, CA (November 2012).
  • Induction, co-induction, calculations—what's not to like about Dafny?
    • Chalmers Technical University, Göteborg, Sweden (May 2013).
    • Imperial College, London, UK (November 2012).
    • CMU, Pittsburgh, PA (November 2012).
  • Dafny, a programming system for functional correctness
    • Oracle Labs, Redwood Shores, CA (May 2013).
    • Ohio State University, Columbus, OH (November 2012).
    • NASA JPL LaRS, Pasadena, CA (November 2012).
  • Staged program development
    • Keynote, SPLASH 2012, Tucson, AZ (October 2012).
  • Coinduction in a language and verifier
    • IFIP WG 2.3 meeting 53, Kirkland, WA (July 2012).
  • Induction and coinduction in an automatic program verifier
    • Dagstuhl seminar on AI meets formal software development, Schloss Dagstuhl, Germany (July 2012).
  • Dafny: a tool for program correctness
    • PL seminar, MIT, Cambridge, MA (June 2012).
  • Languages and tools for supporting programmers at design time
    • Invited talk, New England Programming Languages and Systems Symposium (NEPLS), Portland, ME (June 2012).
  • Engineering Methods for Ensuring Program Correctness
    • Microsoft Research LATAM Faculty Summit, Riviera Maya, Mexico (May 2012).
  • Dafny: A Language and Program Verifier for Functional Correctness
    • Tutorial, Microsoft Research LATAM Faculty Summit, Riviera Maya, Mexico (May 2012).
  • Program verification using Dafny
    • ELLIIT Distinguished Lecture, Linköping University, Linköping, Sweden (March 2012).
  • Wasn't that easy?! A tutorial on program verification with Dafny
    • Tutorial, KTH, Stockholm, Sweden (March 2012).
  • The increasing role of verification in software development
    • ACCESS Distinguished Lecture Series, KTH, Stockholm, Sweden (March 2012).
  • Induction in the program verifier Dafny
    • Imperial College, London, UK (February 2012).
  • Chalice, use and encoding
    • Philippa Gardner's group meeting, Imperial College, London, UK (February 2012).
  • Developing verified programs with Dafny
    • Semantics lunch, Cambridge University, Cambridge, UK (February 2012).
    • Invited tutorial, VSTTE 2012, Philadelphia, PA (January 2012).
  • Using Chalice to reason about objects and concurrency
    • POPL TutorialFest 2012 (x2), Philadelphia, PA (January 2012).
  • Program verification
    • Guest lecture in Ethan Jackson's CSE P 503, University of Washington, Seattle, WA (January 2012).
  • Program synthesis with Jennisys
    • IFIP WG 2.3 meeting 52, Winchester, UK (September 2011).
  • Using and Building an Automatic Program Verifier.  4 or 6 lectures.
    • LASER Summer School 2011, Elba, Italy (September 2011).
    • International Summer School Marktoberdorf, Bayrischzell, Germany (August 2011).
  • Using Program Verification Tools in Teaching
    • With Rajeev Joshi and Rosemary Monahan.  Session, Microsoft Research Faculty Summit, Redmond, WA (July 2011).
  • Harnessing SMT power using the verification engine Boogie
    • SAT/SMT Solver Summer School 2011, MIT, Cambridge, MA (June 2011).
  • Building an SMT-based program verifier using Boogie
    • Informatics@Edinburgh Distinguished Lecture - specialized lecture, Edinburgh, Scotland (May 2011).
  • Program verification Yesterday, today, tomorrow
    • Informatics@Edinburgh Distinguished Lecture, Edinburgh, Scotland (May 2011).
  • From Retrospective Verification to Forward-Looking Development
    • Invited talk, NFM 2011, Pasadena, CA (April 2011).
  • Dafny: A program verifier for functional correctness, and for students
    • University of Lugano, Lugano, Switzerland (February 2011).
    • UT Austin, Austin, TX (January 2011).
  • Refinement, reusable libraries, instantiable classes
    • IFIP WG 2.3 meeting 51, Santa Barbara, CA (January 2011).
  • Tools and Behavioral Abstraction: A Direction for Software Engineering
    • Invited talk, Future of Software Engineering symposium, Zurich, Switzerland (November 2010).
  • Using Boogie 2 in the verification of Spec# programs
    • With Rosemary Monahan.  Tutorial, SBMF 2010, Natal, Brazil (November 2010).
  • Dafny, a program verifier for functional correctness
    • Technical University Eindhoven, Eindhoven, The Netherlands (November 2011).
    • CMU, Pittsburg, PA (April 2011).
    • Seminar, Altran Praxis, Bath, UK (August 2010).
  • The Dafny program verifier
    • Victoria University of Wellington, Wellington, NZ (April 2010).
  • Contracts, tools, verification
    • Keynote, ASWEC 2010, Auckland, NZ (April 2010).
  • Two problems in the specification of termination
    • IFIP WG 2.3 meeting 50, Lachen, Switzerland (March 2010).
  • Verifying Concurrent Programs with Chalice
    • Invited talk, VMCAI 2010, Madrid, Spain (January 2010).
  • Fun with code, tests, and verification
    • Guest lecture in Mani Chandy's CS 141, Caltech, Pasadena, CA (November 2009).
  • Understanding Program Verification
    • Invited talk, PROLE 2009, San Sebastian, Spain (September 2009).
  • Verification of concurrent object-oriented programs
    • EPFL, Lausanne, Switzerland (September 2009).
  • A Foundation for Verifying Concurrent Programs.  2 lectures.
    • 9th International School on Foundations of Security Analysis and Design (FOSAD 2009), Bertinoro, Italy (September 2009).
  • Comparing heap models: Ownership, Dynamic frames, Permissions
    • Dagstuhl seminar on Typing, Analysis and Verification of Heap-Manipulating Programs, Schloss Dagstuhl, Germany (July 2009).
  • Dynamic-frame specifications in Dafny
    • JML seminar, Schloss Dagstuhl, Germany (July 2009).
  • Locks, channels, deadlock freedom, progress
    • IFIP WG 2.3 meeting 49, Boston, MA (June 2009).
  • Correct Concurrency with Chalice
    • Seminar, MIT, Cambridge, MA (June 2009).
    • Seminar, INRIA-MSR joint lab, Orsay, France (January 2009).
  • Verification tools at Microsoft
    • Invited talk, Digiteo seminar, Orsay, France (January 2009).
  • How tool-based verification can be incorporated in teaching
    • Invited talk, Informatics Education Europe III, Venice, Italy (December 2008).
  • Specification techniques for verifying object-oriented software
    • University of Lugano, Lugano, Switzerland (December 2008).
  • Dynamic-frame specifications in Dafny
    • Invited talk, COST Action IC0701, Formal Verification of Object-Oriented Software, working group meeting, Madrid, Spain (December 2008).
  • Specification and Verification of Object-Oriented Software.  5 lectures.
    • International Summer School Marktoberdorf, Marktoberdorf, Germany (August 2008).
  • Ceaselessly-analyzing development environments
    • Panel presentation, COMPSAC 2008, Turku, Finland (July 2008).
  • Specification and Verification of Programs with Pointers.  2 lectures.
    • Summer School on Logic and Theorem-Proving in Programming Languages, Eugene, OR (July 2008).
  • Thread-local contributions
    • IFIP WG 2.3 meeting 48, Cambridge, UK (July 2008).
  • Spec#
    • Alt.NET, Redmond, WA (April 2008).
  • Boogie
    • Microsoft Research India, Bangalore, India (February 2008).
  • Program verification using the Spec# programming system
    • With Rosemary Monahan.  Tutorial, ETAPS 2008, Budapest, Hungary (March 2007).
  • Specifying and verifying software
    • KU Leuven, Leuven, Belgium (August 2008).
    • Chalmers, Göteborg, Sweden (November 2007).
    • Invited talk, ASE 2007, Atlanta, GA (November 2007).
  • Spec#
    • Invited talk, Øredev, Malmö, Sweden (November 2007).
  • Designing a type system for BoogiePL 2
    • IFIP WG 2.3 meeting 47, Santa Fe, NM (October 2007).
  • Designing verification conditions for software
    • Invited talk, CADE-21, Bremen, Germany (July 2007).
  • Program verification via an intermediate language
    • Seminar, National University of Ireland, Maynooth, Maynooth, Ireland (June 2007).
  • Verifying object-oriented software: Lessons and challenges
    • Invited talk, TACAS 2007, part of ETAPS in Braga, Portugal (March 2007).
  • Reasoning about object structures in Spec#
    • UNSW, Sydney, Australia (January 2007).
    • INRIA + Microsoft lab, Paris, France (November 2006).
  • Automatic verification of summations
    • IFIP WG 2.3 meeting 46, Sydney, Australia (January 2007).
  • Going beyond a simple ownership system in Spec#
    • European Science Foundation workshop on Java program verification, Nijmegen, The Netherlands (October 2006).
  • Object invariants in specification and verification
    • Invited talk, Brazilian Symposium on Formal Methods (SBMF 2006), Natal, Brazil (September 2006).
  • Spec#
    • Microsoft Research Faculty Summit 2006, Redmond, WA (July 2006).
  • Specifying and verifying programs in Spec#.
    • Invited talk, Sixth International Andrei Ershov Memorial Conference Perspectives of System Informatics (PSI 2006), Novosibirsk, Russia (June 2006).
  • Building a program verifier
    • Guest lecture in Shaz Qadeer's CSE 599f, Formal Verification of Computer Systems, University of Washington, Seattle, Washington (May 2006).
  • Panel on Integrated Verification
    • The Challenge of Software Verification, Schloss Dagstuhl, Germany (Jul 2006).
    • IFIP WG 2.3 meeting 45, Bruges, Belgium (April 2006).
  • Invariants on demand
    • Invited talk, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), Koblenz, Germany (September 2005).
  • Loop invariants on demand
    • IFIP WG 2.3 meeting 44, Niagara Falls, ON (June 2005).
  • The Spec# programming system
    • Distinguished Lecture, Max-Planck Institute for Software Systems, Kaiserslautern, Germany (March 2006).
    • Seminar, Åbo Akademi University, Turku, Finland (December 2005).
    • Lunch seminar, Praxis High Integrity Systems, Bath, UK (December 2005).
    • Short presentation and demo, Verified Software: Theories, Tools, Experiments (VSTTE 2005), Zurich, Switzerland (October 2005).
    • Software Quality Research Lab Distinguished Lecture, McMaster University, Hamilton, ON (May 2005).
    • Colloquium, University of Toronto, Toronto, ON (May 2005).
  • Advanced programming tools at Microsoft
    • Distinguished Lecture, York University, Toronto, ON (May 2005).
  • Demand-driven inference of loop invariants in a theorem prover.
    • Invited talk, Fourth International Workshop on Automated Verification of Infinite-State Systems (AVIS'05), Edinburgh, Scotland, UK (April 2005).
  • Program verification and programming methodology.
    • Invited talk, 12th International Workshop on Abstract State Machines (ASM 2005), Paris, France (March 2005).
  • Programming methodology.
    • Panel discussion, Workshop on the Verification Grand Challenge, Menlo Park, CA (February 2005).
  • Writing specifications for object-oriented programs.
    • Invited talk, First International Workshop on Abstract Interpretation of Object-Oriented Languages, Paris, France (January 2005).
  • Challenges in increasing tool support for programming.
    • Invited talk, First International Colloquium on Theoretical Aspects of Computing, Guiyang, Guizhou, China (September 2004).
  • On bounded model checking, induction, and interpolants
    • IFIP WG 2.3 meeting 43, Prato, Italy (September 2004).
  • Spec#: Writing and checking contracts in a .NET language.
    • Keynote, .NET Technologies 2004, 2nd International Workshop, Plzeň, Czech Republic (June 2004).
  • Hoare-style program verification.  3 lectures.
    • Guest lectures in Rob DeLine's CSE 503, Software Engineering, University of Washington, Seattle, Washington (April/May 2004).
  • Toward enforceable contracts in .NET
    • Keynote, Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS 2004), Marseille, France (March 2004).
  • Abstract interpretation for heap structures
    • IFIP WG 2.3 meeting 42, Philadelphia, PA (January 2004).
  • Verifying invariants in object-oriented programs
    • Colloquium, Department of Computer Science, ETH Zurich, Switzerland (November 2003).
  • Technologies for finding errors in object-oriented software.  4 lectures.
    • UNU-IIST (United Nations University - International Institute for Software Technology) and IFIP WG 2.3 Summer School on Formal methods of Software, Tunis, Tunisia (September 2003).
  • Static program checking, module by module
    • Invited tutorial, Prato workshop on Trusted Components, Prato, Italy (January 2003).
  • A SAT characterization of boolean-program correctness.
    • IFIP WG 2.3 meeting 41, Biarritz, France (March 2003).
    • Department colloquium, Washington University in St. Louis, St. Louis, MO (February 2003).
    • IFIP WG 2.4 meeting, Schloss Dagstuhl, Germany (November 2002).
    • University of Eindhoven, Eindhoven, The Netherlands (November 2002).
  • ESC/Java or Light-weight formal methods: from objects to components. 
    • Invited talk, First international symposium on Formal Methods for Components and Objects (FMCO 2002), Leiden, The Netherlands (November 2002).
  • Checking correctness properties of object-oriented programs.  5 lectures.
    • EEF Summer School on Specification, Refinement and Verification, Turku, Finland (August 2002).
  • Modular checking and side effects.
    • IFIP WG 2.3 meeting 40, Turku, Finland (August 2002).
  • Checking side effects in object-oriented programs.
    • Invited talk, Java Verification Workshop (JVW'02), Portland, OR (January 2001).
  • ESC/Java: The Greatest Thing Since Sliced Bread.
    • Distinguished Lecturer Series, Computing and Information Sciences, Kansas State University, Manhattan, KS (October 2001).
  • Applications of extended static checking.
    • Invited talk, Static Analysis Symposium (SAS'01), Paris, France (July 2001).
  • Challenging applications of extended static checking.
    • Panelist, Silver bullets for AI softwolves, AAAI 2001 Spring Symposium on Model-Based Validation of Intelligence, Stanford, CA (March 2001).
  • Houdini, an annotation assistant for ESC/Java. 
    • Swedish Institute of Computer Science, Kista, Sweden (May 2001).
    • Uppsala University, Uppsala, Sweden (May 2001).
    • Chalmers University of Technology, Göteborg, Sweden (May 2001).
    • Computer science colloquium, University of Iowa, Iowa City, IA (May 2001).
    • Microsoft Research, Redmond, WA (April 2001).
    • Imperial College, London, England (January 2001).
    • Oxford University, Oxford, England (January 2001).
  • Benevolent side effects considered malevolent.
    • IFIP WG 2.3 meeting 38, Santa Cruz, CA (January 2001).
  • Program checking. 
    • Invited talk, Schloss Dagstuhl's Tenth Anniversary conference Informatics—10 years back, 10 years ahead, Saarbrucken, Germany (August 2000).
    • IFIP WG 2.3 workshop on program methodology, Tandil, Argentina (September 2000).
  • Real estate of names.
    • Invited talklet, In Pursuit of Simplicity, a symposium honoring Edsger W. Dijkstra, UT Austin, Austin, TX (May 2000).
  • Extended static checking for Java. 
    • Automated Software Engineering Group seminar, NASA Ames, Mountain View, CA (November 2001).
    • Distinguished Lecture Series, Cornell University Computer Science Department, Ithaca, NY (Oct 2001).
    • University of Toronto, Toronto, ON, Canada (May 2001).
    • Computer Science Seminar, University of Cambridge, Cambridge, England (April 2000).
    • LFCS Theory Seminar, University of Edinburgh, Edinburgh, Scotland (April 2000).
    • University of Glasgow, Glasgow, Scotland (April 2000).
    • Programming Systems Seminar, UC Berkeley, Berkeley, CA (March 2000).
    • UC Davis, Davis, CA (February 2000).
  • Finding bugs in Java programs. 
    • IFIP WG 2.3 meeting 37, Longhorsley, England (April 2000).
  • ESC/Java. 
    • Stanford University, Stanford, CA (October 1999).
    • Invited talk, Larch Users' Group Meeting at World Congress on Formal Methods (FM'99), Toulouse, France (September 1999).
    • UW/MSR Summer Institute on Technologies to Improve Software Development, Semi-ah-moo, WA (August 1999).
  • The essence of object-oriented program semantics.
    • Distinguished Lecturer Series - specialized lecture, Computing and Information Sciences, Kansas State University, Manhattan, KS (October 2001).
    • The University of Texas at Austin, Austin, TX (October 1999).
    • The semantic challenge of object-oriented programming (seminar), Schloss Dagstuhl, Germany (June 1998).
    • IFIP WG 2.3 meeting 35, Bloomington, IN (June 1998).
  • Extended static checking. 
    • Invited talk, PROCOMET'98, Shelter Island, NY (June 1998).
  • A semantic approach to secure information flow. 
    • California Institute of Technology, Pasadena, CA (March 1998).
    • IFIP WG 2.3 meeting 34, Alsace, France (September 1997).
  • Soundness and completeness considered harmful. 
    • SRI computer science seminar, Menlo Park, CA (May 1998).
  • Object invariants in Java. 
    • IFIP WG 2.3 meeting 34, Alsace, France (September 1997).
  • Generalized data abstraction. 
    • IFIP WG 2.3 meeting 33, Napa Valley, CA (January 1997).
  • Extended static checking. 
    • ETH Zurich, Zurich, Switzerland (September 1997).
    • The University of Texas at Austin, Austin, TX (August 1997).
    • Rice University, Houston, TX (July 1997).
    • IBM Austin Research Laboratory, Austin, TX (July 1997).
    • Seminar on semantics and abstract interpretation, Ecole Normale Superieure, Paris, France (April 1997).
    • California Institute of Technology, Pasadena, CA (December 1996).
    • Odyssey Research Associates, Inc., Ithaca, NY (November 1996).
    • NUPRL seminar, Cornell University, Ithaca, NY (November 1996).
  • Toward reliable modular programs. 
    • Microsoft Research, Redmond, WA (January 1995).

Professional distinctions

  • IFIP Fellow, 2022
  • ACM Fellow, 2016
  • Tool Used by Most Teams Award (for Dafny), VerifyThis @ ETAPS 2015 program verification competition
  • ACM SIGPLAN Most Influential 2002 PLDI Paper Award, 2012.  For the paper "Extended Static Checking for Java" by Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.
  • Shared Tool Used by Most Teams Award (for Dafny), VerifyThis @ FM 2012 program verification competition
  • Silver Medal (with Peter Müller), VSTTE 2012 Program Verification Competition
  • Best Paper Award, FM 2011 for the paper "Software Competition: Experience Report" by Vladimir Klebanov, et al.
  • IFIP Silver Core Award, 2010, awarded for outstanding service
  • Member, IFIP Working Group 2.3 "Programming Methodology", 2000-present.  (Secretary, 2003-2012.) (Vice Chair, 2014-2020.) (Chair, 2020-present.)

Graduate school awards and distinctions

  • Research supported by Digital Equipment Corporation Systems Research Center, Palo Alto, CA, 1992-93 and 1994-95.
  • American Scandinavian Foundation of Los Angeles. Scholarship, 1994.
  • One of about 75 computer science students selected worldwide to attend the International Summer School on Program Design Calculi, Marktoberdorf, Germany, 1992.

Undergraduate awards and distinctions

  • Upsilon Pi Epsilon, Computer Science Honors Society (elected officer, UT Austin, 1988-89).
  • College of Natural Sciences, College Scholar, UT Austin, 1988 and 1989.
  • The Honor Society of Phi Kappa Phi.
  • Phi Beta Kappa.
  • Golden Key National Honor Society.
  • Angus G. and Erna H. Pearson Endowed Scholarship, UT Austin, 1988.
  • Alpha Lambda Delta, Freshman Honor Society.
  • Phi Eta Sigma, Freshman Honor Society.

High school awards and distinctions

  • Among numerous other academic high school awards, won 1st place Advanced Level, Kentucky Council Teachers of Mathematics High School Math Contest, 1985-86.
  • Among other high school programming contests first places, tied 5th place in the 1986 International Computer Program Solving Contest, in which 2500 teams from 13 countries participated. (With team mates Robert S. French and Dean Brooks.)
  • Among several other musical awards in high school, selected to play in the 1986 Kentucky All-State Symphonic Band. (Bass saxophone and baritone saxophone.)

Advisory committees

Thesis committees

  • Habilitation thesis committees:
    • Jean-Christophe Filliâtre, Université Paris Sud 11 (December 2011).
    • Claude Marché, University Paris 11 (2005).
  • PhD thesis committees:
    • Jatin Arora, CMU (August 2024).  Advisor: Umut A. Acar.
    • Tim Woods, Imperial College London (December 2016).  Internal reviewer.  Advisor: Sophia Drossopoulou.
    • Martin Hentschel, TU Darmstadt (March 2016).  External reviewer.  Advisor:  Reiner Hähnle.
    • Nadia Polikarpova, ETH Zurich (April 2014).  External reviewer.  Advisor:  Bertrand Meyer.
    • Nicholas Smallbone, Chalmers Technical University (May 2013).  Opponent.  Advisor:  Koen Claessen.
    • Ronald Middelkoop, Technical University Eindhoven (November 2011).  External reviewer.  Advisor: Ruurd Kuiper and Kees Huizing.  Professor:  Mark G. J. van den Brand.
    • Aliaksei Ttsitovich, University of Lugano (February 2011).  Advisor: Natasha Sharygina.
    • Radu Grigore, University College Dublin (August 2010).  External reviewer.  Advisor:  Joe Kiniry.
    • Yannick Moy, Université Paris 11 (2009).  External reviewer.  Advisor: Claude Marché.
    • Cristina Cerschi Seceleanu, Åbo Akademi University (2005).  External reviewer and Opponent.  Advisor:  Academy Prof. Dr. Ralph-Johan Back.
    • Rajeev Joshi, The University of Texas at Austin (1999).  Advisor:  Prof. Dr. Jayadev Misra.

Editorial boards

  • Editorial board, Journal of Automated Reasoning, 2007-present.

Project advice

  • Project evaluator, Research theme: Proof and Verification, INRIA, 2015.
  • Project evaluator, Research theme A: Symbolic systems, INRIA, 2006.
  • Scientific advisory board, Mobius project, 2005-2007.
  • Project retreat external visitor, Open Software Quality project, UC Berkeley, May 2001.

Steering committees

  • Programming Languages meet Program Verification (PLPV) workshop (2011-2015)
  • ETAPS steering committee (2011-2012)
  • BOOGIE workshop on intermediate verification languages (2011-2012)
  • Formal Techniques for Java-like Programs (FTfJP) workshop (2004-present)

Program committees

  • 13th International Conference on integrated Formal Methods (iFM 2017), Torino, Italy (September 2017).
  • 29th International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany (July 2017).
  • Formal Methods (FM 2016), Limassol, Cyprus (November 2016).
  • 3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), at FM 2016, Limassol, Cyprus (November 2016).
  • 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), Toronto, ON, Canada (July 2016).
  • Co-chair, International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2016), St Petersburg, FL, USA (January 2016).
  • 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-20), Suva, Fiji (November 2015).
  • Formal Methods (FM 2015), Oslo, Norway (June 2015).
  • 7th NASA Formal Methods Symposium (NFM 2015), Pasadena, CA, USA (April 2015).
  • 2nd Workshop on Formal Integrated Development Environment (F-IDE 2015), at FM 2015, Oslo, Norway (June 2015).
  • 1st Workshop on Formal Integrated Development Environment (F-IDE 2014), at ETAPS 2014, Grenoble, France (April 2014).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2013), at ECOOP 2013, Montpellier, France (2013).
  • ESEC/FSE 2013 Tool Demos (ESEC/FSE Tools), Saint Petersburg, Russia (August 2013).
  • 24th International Conference on Automated Deduction (CADE-24), Lake Placid, NY (June 2013).
  • 27th European Conference on Object-Oriented Programming (ECOOP 2013), Montpellier, France (June 2013).
  • Formal Methods (FM 2012), Paris, France (August 2012).
  • 26th European Conference on Object-Oriented Programming (ECOOP 2012), Beijing, China (June 2012).
  • Eighteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Tallinn, Estonia (March 2012).
  • Verified Software: Theories, Tools and Experiments (VSTTE 2012), Philadelphia, PA (January 2012).
  • Co-chair, First International Workshop on Intermediate Verification Languages (BOOGIE 2011), Wrocław, Poland (August 2011).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2011), Lancaster UK (July 2011).
  • Co-chair, Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), Saarbrücken, Germany (March-April 2011).
  • Verified Software: Theories, Tools and Experiments (VSTTE 2010), Edinburgh, Scotland (August 2010).
  • International Joint Conference on Automated Reasoning (IJCAR 2010), Edinburgh, Scotland (July 2010).
  • Programming Languages meets Program Verification (PLPV 2010), Madrid, Spain (January 2010).
  • Verification, Model Checking, and Abstract Interpretation (VMCAI 2010), Madrid, Spain (January 2010).
  • 11th International Conference on Formal Engineering Methods (ICFEM 2009), Rio de Janeiro, Brazil (December 2009).
  • International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO 2009) (July 2009).
  • Seventh International Andrei Ershov Memorial Conference, Perspectives of System Informatics (PSI 2009), Novosibirsk, Russia (June 2009).
  • Programming Languages meets Program Verification (PLPV 2009), Savannah, Georgia (January 2009).
  • 15th International Symposium on Formal Methods (FM 2008), Turku, Finland (May 2008).
  • Verification, Model Checking, and Abstract Interpretation (VMCAI 2008), San Francisco, CA (January 2008).
  • Ninth International Conference on Formal Engineering Methods (ICFEM 2007), Boca Raton, FL, USA (November 2007).
  • International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO 2007), at ECOOP 2007, Berlin, Germany (July 2007).
  • Workshop on Programming Languages and Analysis for Security (PLAS 2007), at PLDI 2007, San Diego, CA, USA (June 2007).
  • International Conference TOOLS EUROPE 2007 - Objects, Models, Components, Patterns, Zurich, Switzerland (June 2007).
  • Foundations and Developments of Object-Oriented Languages (FOOL/WOOD 2007), at POPL 2007, Nice, France (January 2007).
  • Co-chair, Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2006), at FLoC 2006, Seattle, WA, USA (August 2006).
  • Formal Methods (FM 2006), Hamilton, Canada (August 2006).
  • 15th International Conference on Compiler Construction (CC 2006), Vienna, Austria (March 2006).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2006), at ECOOP, Nantes, France (July 2006).
  • Fourth workshop on Specification and Verification of Component-Based Systems (SAVCBS 2005), at ESEC/FSE 2005, Lisbon, Portugal (September 2005).
  • 3rd International Conference on Software Engineering and Formal Methods (SEFM 2005), Koblenz, Germany (September 2005).
  • 1st International Workshop on Abstract Interpretation of Object-Oriented Languages (AIOOL), at VMCAI 2005, Paris, France (January 2005).
  • 14th International Conference on Compiler Construction (CC 2005), Edinburgh, Scotland (April 2005).
  • Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2004), at ACM SIGSOFT 2004/FSE-12, Newport Beach, California (October/November 2004).
  • 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), Beijing, China (September 2004).
  • Mathematics of Program Construction (MPC 2004), Stirling, Scotland, UK (July 2004).
  • 2nd International Workshop on .NET Technologies'2004, University of West Bohemia, Campus-Bory Plzen, Czech Republic (31 May - 2 June 2004).
  • Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2003), at ESEC/FSE, Helsinki, Finland (September 2003).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2003), at ECOOP, Darmstadt, Germany (July 2003).
  • Prato workshop on Trusted Components, Prato, Italy (January 2003).
  • Workshop on Formal Techniques for Java-like Programs (FTfJP 2002), at ECOOP, Málaga, Spain (June 2002).
  • Workshop on Foundations of Aspect-oriented Languages (FOAL), at AOSD, Enschede, The Netherlands (April 2002).
  • Mathematics of Program Construction (MPC 2002), Schloss Dagstuhl, Germany (July 2002).
  • ACM Symposium on Principles of Programming Languages (POPL'02), Portland, Oregon (January 2002).
  • Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2001), at OOPSLA, October 2001.
  • Workshop on Formal Techniques for Java Programs (FTfJP 2001), at ECOOP, Budapest, Hungary (June 2001).
  • The Second International Workshop on Automated Program Analysis, Testing and Verification (WAPATV), at ICSE, Toronto, Canada (May 2001).
  • Mathematics of Program Construction (MPC 2000), Ponte de Lima, Portugal, July 2000.
  • The First International Workshop on Automated Program Analysis, Testing and Verification (WAPATV), at ICSE, University of Limerick, Ireland, June 2000.
  • Intercontinental Workshop on Aliasing in Object-Oriented Systems (IWAOOS'99), in conjunction with ECOOP, Lisbon, Portugal, June 1999.
  • The Sixth International Workshop on Foundations of Object-Oriented Languages (FOOL 6), at POPL, San Antonio, TX, January 1999.

External Review Committees

  • 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), External Review Committee, Rome, Italy.

Mentoring

  • Intern mentor, Amazon Web Services:
    • Tabea Bordis (KIT), 2023.
    • Gaurav Parthasarathy (ETH Zurich), 2022.
    • Stefan Zetzsche (University College London), 2021.
    • Jatin Arora (CMU), 2021.
    • Wouter Schols (Eindhoven University of Technology), 2020.
    • Marianna Rapoport (U. Waterloo), 2019.
    • Sam Gruetter (MIT), 2019.
    • Vihang Patel (Texas A&M), 2019.
    • Jared Lim (Cornell), 2019.
    • Joshua Gancher (Cornell), 2019.
    • Matthias Schlaipfer (TU Vienna), 2019.
    • Daniel Schoepe (Chalmers), 2018.
    • Steven S. Lyubomirsky (U. Washington), 2018.
    • James Bornholt (U. Washington), 2018.
  • Research intern mentor, Microsoft Research:
    • James Wilcox (U. Washington), shared intern with Jay Lorch, 2017.
    • Daniel Matichuk (Software Systems Research Group at Data61), 2016.
    • Kenny Foner (U. Penn), 2016.
    • Clément Pit--Claudel (MIT), 2015.
    • Dan Rosén (Chalmers), 2014.
    • Maria Christakis (ETH Zurich), 2013.
    • Valentin Wüstholz (ETH Zurich), 2013.
    • Jason Koenig (CMU), 2011, 2012.
    • Aleksandar Milicevic (MIT), 2011.
    • Kuat Yessenov (MIT), 2010.
    • Claire Le Goues (U. Virginia), 2009.
    • Philipp Rümmer (Chalmers), 2008, 2009.
    • Ronald Middelkoop (TU Eindhoven), 2007.
    • Ralf Sasse (UI Urbana-Champaign), 2007.
    • Ádám Darvas (ETH Zurich), 2006.
    • Angela Wallenburg (Chalmers), 2006.
    • Bor-Yuh Evan Chang (UC Berkeley), 2004, 2005.
    • Xinming Ou (Princeton), 2004.
    • Rob Klapper (Washington University in St. Louis), 2003.
    • Viktor Kuncak (MIT), 2002.
  • Mentor, Compaq SRC:
    • Stephen N. Freund, 2000-2001.
    • Rajeev Joshi, 1999-2001.
    • Cormac Flanagan, 1997-2001.
    • Raymie Stata, 1996-2000.
  • Research intern host, Compaq SRC:
    • Todd Millstein (University of Washington), 1999.
    • Rajeev Joshi (The University of Texas at Austin), 1997.

Other professional activities

  • Delegate, National Academy of Engineering / UK Royal Academy of Engineering / Chinese Academy of Engineering Global Grand Challenges Summit, Washington, DC, USA, 2018.
  • Delegate, National Academy of Engineering / UK Royal Academy of Engineering / Chinese Academy of Engineering Global Grand Challenges Summit, Beijing, China, 2016.
  • Microsoft Achievement Award (awarded 2011, used Aug-Oct 2013)
  • Delegate, National Academy of Engineering / UK Royal Academy of Engineering / Chinese Academy of Engineering Global Grand Challenges Summit, London, UK, 2013.
  • National Academy of Engineering Japan-America Frontiers of Engineering symposium, Irvine, CA, Nov 2009.
  • National Academy of Engineering Frontiers of Engineering symposium, Redmond, WA, 2007.
  • Summer intern czar (program coordinator), Compaq SRC, 1998.
  • Graduate Admissions Committee, Computer Science, Caltech, 1994.
  • Contributing editor to Cobb Journal on Microsoft Word for the PC, 1990-1991.
  • Contributor to the LAN Manager Programming Reference, Microsoft Press, 1990.
  • Member of the Association for Computing Machinery, 1989-present.

Patents

  • Cormac Andrias Flanagan and K. Rustan M. Leino.  Method and apparatus for automatically inferring annotations.  U.S. Patent 7,120,902, October 2006.
  • K. Rustan M. Leino, Todd David Millstein, and James B. Saxe.  System and method for verifying computer program correctness and providing recoverable execution trace information.  U.S. Patent 7,024,661, April 2006.
  • Cormac Andrias Flanagan and K. Rustan M. Leino.  Method and apparatus for organizing warning messages.  U.S. Patent 6,978,443, December 2005.
  • Raymond Paul Stata, Cormac Flanagan, K. Rustan M. Leino, Mark D. Lillibridge, and James Benjamin Saxe.  System and method for lexing and parsing program annotations.  U.S. Patent 6,353,925, March 2002.
  • K. Rustan M. Leino, Mark David Lillibridge, and Raymond Paul Stata. Method and apparatus for statically analyzing a computer program for data dependencies. U.S. Patent 5,987,252, November 1999.

Shareware computer games

Compact Discs

  • Caltech Jazz Bands. Exothermic Jazz. 1994.  Director:  Bill Bing. (Tenor and baritone saxophones.)

Videos and soundtracks

  • Verification Corner (http://research.microsoft.com/verificationcorner)
  • PPRC Summer Intern Video, The Incredible Race.  Microsoft Research, 2003.  (Production.  And with others, editing and soundtrack.)
  • PPRC Espresso Machine Tutorial.  Microsoft Research, 2003.  With Shaz Qadeer.
  • PPRC Summer Intern Video, Episode 2002: Attack of the aliasing bug.  Microsoft Research, 2002.  (Production.  And with others, editing and soundtrack.)
  • Soundtrack for Emergency Response Procedures video, Compaq SRC, 2000.
  • Soundtrack for Compaq Research for Palo Alto Chamber of Commerce, 2000.
  • Soundtrack for SRC Summer Intern Video 1999. (With Todd Millstein.)
  • Soundtrack for research videos At the Gallery and In the Lab, describing the Bytes of Art project, 1998.
  • Soundtrack for research video describing VistaBar, 1997.
  • SRC Summer Intern Video 1994. (Script, soundtrack, and editing, joint with others.)
  • SRC Summer Intern Video 1992. (Soundtrack and editing, joint with others.)

Acknowledgment: Ken Beckman made the videos in the third group above possible and lots of fun.

Original music

Some recordings, lyrics, and sheet music of original music is available at https://leino-online.com/music.

Some musical appearances

  • Various bands, St. Matthew's Lutheran Church, Renton, WA.  2012-present.  (Drums, bass, keyboards, tenor sax.)
  • House band, retirement party, Luther's Table, Renton, WA.  July 2016.  (Bass.)
  • House band, Children's Hospital Cancer Research fund raiser, Mercer Island, WA.  October 2012.  (Drums.)
  • Jazz Open Jam, a monthly event, Luther's Table, Renton, WA.  2012-2013.  (Drums, keyboards, tenor sax, vocals.)
  • Principles of Jazz, POPL 2012 jazz band, Philadelphia, PA.  January 2012.  (Drums, piano.)
  • Farewell party band, Marktoberdorf International Summer School, Bayrischzell, Germany, 2011.  (Piano, vocals.)
  • Principles of Jazz, POPL 2011 jazz band, Austin, TX.  January 2011.  (Drums, tenor sax, piano.)
  • The Assumptions, Marktoberdorf International Summer School, Marktoberdorf, Germany, 2008.  (Tenor sax, bass, keyboards, drums.)
  • God's Garage band, every third Sunday at 9:30 and 11:00 services, St. Matthew's Lutheran Church, Renton, WA.  2008-2011.  (Drums, fill-in on keyboards.)
  • Song of the day, monthly at 10:30 service, with Grace Ensemble.  Grace Lutheran Church, Bellevue, WA.  2002-2005.  (Drums, bass guitar, keyboards, sax.)
  • Weekly worship services, Immanuel Lutheran Church, Los Altos, CA. 1996-2001. (Drums, bass guitar, keyboards, vocals.)
  • Joseph and the technicolor dreamcoat. St. Lawrence Academy, March 2001. (Drums.)
  • They're playing our song. West Valley Light Opera, Spring 1999. (Drums.)
  • Various concerts with the Caltech Thursday Jazz Band, 1992-95. Guest artists at concerts included: drummer Gregg Bissonette, guitarist Grant Geissman, trumpet player Chuck Findley, vocalist Angie Whitney, and composer and arranger Joe Curiale. (Tenor and baritone saxophones.)
  • Various concerts with the Caltech Monday Jazz Band, 1991-92. (Tenor saxophone.)
  • Special appearance with rock band Bob Popular, UT Austin, May 1989. (Tenor saxophone.)

Some extracurricular activities

  • Sabbatical team, St Matthew's Lutheran Church, Renton, WA. (2023)
  • Mutual Ministry Team, St Matthew's Lutheran Church, Renton, WA. (2022-present)
  • Board member, Mending Wings, Yakama Nation. (September 2013-December 2016)
  • Volunteer, Luther's Table (a cafe and bar), Renton, WA. (September-October 2013)
  • Volunteer High School math teacher, Maths Camp, Sponsor an African Scholar (SAAS), Mombasa, Kenya. (August 2013)
  • Vice President, St. Matthew's Lutheran Church, Renton, WA.  (2013-present)
  • Council member, St. Matthew's Lutheran Church, Renton, WA.  (2012-present)
  • Group Exercise Volunteer (step aerobics instructor), Bellevue Family YMCA, Bellevue, WA.  2004-2012.  (Substitute instructor, 2012-2017.)
  • Celebrity scientist, 2nd grade class, Somerset Elementary School, Bellevue, WA, January 2007.
  • Celebrity scientist, one 1st grade and one 4th grade class, Somerset Elementary School, Bellevue, WA, February 2006.
  • Fusion Jazz combo (drums), Ron Cole, instructor, Music Works Northwest, Spring 2005, Fall 2005, Winter 2006, Spring 2006.
  • Smooth Jazz combo (drums), Darren Motamedy, instructor, Music Works Northwest, Fall 2004, Winter 2005.
  • Chair, Evangelism committee, Grace Lutheran Church, Bellevue, WA.  2004-present.
  • Coach of a Somerset Elementary School team for Middle School Math Olympiad, Bellevue, WA, Spring 2004.
  • Music leader, Grace Ensemble, Grace Lutheran Church, Bellevue, WA.  2002-2005.
  • Worship and music committee, Grace Lutheran Church, Bellevue, WA.  2002-2004.
  • Co-coach of a Somerset Elementary School team for Middle School Math Olympiad, Bellevue, WA, Spring 2002.
  • Co-leader, small-group Bible studies (Genesis; Jeremiah; Romans; Revelation; Shadow of the Galilean; The inward pilgrimage: an introduction to Christian spiritual classics), Immanuel Lutheran Church, Los Altos, CA, 1999-2001.
  • Chair, Evangelism committee, Immanuel Lutheran Church, Los Altos, CA, 1999-2001.
  • Performed and recorded music for youth group musicals, Immanuel Lutheran Church, Los Altos, CA, 1999, 2000.
  • Visioning for the 21st Century committee, Immanuel Lutheran Church, Los Altos, CA, 1999.
  • Church Council, Immanuel Lutheran Church, Los Altos, CA, 1996-1999.
  • Chair, Youth director search committee, Immanuel Lutheran Church, Los Altos, CA, 1997.
  • Music leader, contemporary worship service, Immanuel Lutheran Church, Los Altos, CA, 1996-1997.
  • Representative at ELCA Sierra Pacific Synod convention, 1997.
  • Chair, Second Phase Building Fund Campaign, Immanuel Lutheran Church, Los Altos, CA, Summer 1996.
  • Helped start contemporary worship service, Immanuel Lutheran Church, Los Altos, CA, 1996.
  • Vision 2000 committee, Immanuel Lutheran Church, Los Altos, CA, 1995.
  • Organizer and co-founder, Caltech Swedish Club, Pasadena, CA, 1993-1994.
  • President, AAL Branch #6905 (a fraternal benefit society), San Gabriel, CA, 1993-1994.
  • Arranged, performed, and recorded music for youth group musicals, Trinity Lutheran Church, San Gabriel, CA, 1992, 1993.

Last updated April 2023.