K. Rustan M. Leino

Outline:

• Principal Researcher, Microsoft Research
• Office address:  Microsoft Research, One Microsoft Way, Redmond, WA 98052, USA.
• Email: 
• Work home page:  http://research.microsoft.com/~leino
• Personal home page:  http://leino-online.com
• Wonderfully married, 4 great children.

Programming and program design technologies, programming languages and systems, programming methodology, object-oriented programming, programming tools, specification and verification, program semantics.

Other interests:  music and audio, game programming.

(I'm afraid this list is not as up-to-date or useful as it could be.)

• Dafny, an object-based language and verifier that explores the specification style of dynamic frames.
• VerifiedC (vcc), a static program verifier for systems code written in C.  Joint work with Wolfram Schulte and others.
• Boogie, a static program verifier for .NET.  2003-current.  Joint work with Mike Barnett, Bor-Yuh Evan Chang (UC Berkeley), Bart Jacobs (Katholieke Universiteit Leuven), Francesco Logozzo (Ecole Polytechnique), Peter Müller (ETH Zurich), and others.
• Spec#, a programming language with specifications.  2003-current.  Joint work with Mike Barnett, Bart Jacobs (Katholieke Universiteit Leuven, Belgium), Robert DeLine, Manuel Fähndrich, Wolfram Schulte, and Herman Venter.
• Houdini, a program annotation inference system for ESC/Java.  1999-2001.  Joint work with Cormac Flanagan, Rajeev Joshi, Michael Y. Levin, and Yuan Yu.
• Extended Static Checking for Java.  ESC/Java is a formal-methods based programming tool for finding software defects in Java programs.  Project leader, 1997-2001.  Joint work with Cormac Flanagan, Rajeev Joshi, Mark Lillibridge, Todd D. Millstein, Greg Nelson, James B. Saxe, Raymie Stata, and Caroline Tice.
• Extended Static Checking for Modula-3. An earlier Extended Static Checking project.  1994-1996.  Joint work with David L. Detlefs, Greg Nelson, James B. Saxe, and Rajeev Joshi.
• Wrote video driver for the IT, an early network computer.  1996.
• The 10,000 km Xilinx chip, a piece of hardware for testing long-distance ATM networks.  1995-1996.  Joint work with Hal Murray.
• Modula-3D, a programming language, compiler, and run-time system for programming multicomputers.  SRC and Caltech, 1992-1993.

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

• December 2001 - present.  Principal Researcher (2007 - present), Senior Researcher (2006 - 2007), Researcher (2001-2006).  Microsoft Research, Redmond, WA.
• January 1995 - November 2001.  Computer science researcher.  Compaq Systems Research Center, Palo Alto, CA.
• Spring 1994, Fall 1994.  Co-instructor, Mathematics of Program Construction.  California Institute of Technology, Pasadena, CA.
• Fall 1991 - Fall 1994.  Graduate research assistant.  California Institute of Technology, Pasadena, CA.
• Summer 1994.  Research intern.  Digital Equipment Corporation Systems Research Center, Palo Alto, CA.
• Fall 1991 - Spring 1994.  Teaching assistant, Computation, Computers, Programs.  California Institute of Technology, Pasadena, CA.
• Summer 1992.  Research intern.  Digital Equipment Corporation Systems Research Center, Palo Alto, CA.
• June 1989 - August 1991.  Software design engineer, technical lead.  Microsoft, Redmond, WA.
• February 1988 - May 1989.  President.  CompuGuide, Austin, TX.
• September 1987 - May 1989.  Instructor of computer classes.  Informal Classes, UT Austin, Austin, TX.
• August 1987 - May 1989.  Programmer.  One-Eleven, Inc., Austin, TX.

	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, to appear.
	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, to appear. A previous version appears as Technical Report 06-14, Department of Computer Science, Iowa State University, May 2006.
	Efficient weakest preconditions		IPL
	K. Rustan M. Leino
		Information Processing Letters, 93(6):281-288, March 2005.
	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.
	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.
	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.
	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.
	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.
	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.
	Real estate of names		IPL
	K. Rustan M. Leino
		Information Processing Letters, 77(2-4):169-171, February 2001.
	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.
	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.
	Joining specification statements		TCS
	K. Rustan M. Leino and Rajit Manohar
		Theoretical Computer Science, 216(1-2):375-394, March 1999.
	Computing permutation encodings		FAC
	K. Rustan M. Leino
		Formal Aspects of Computing, 11(1):56-74, 1999.
	Recursive object types in a logic of object-oriented programs		NJC
	K. Rustan M. Leino
		Nordic Journal of Computing, 5(4):330-360, 1998.
	Conditional composition		FAC
	Rajit Manohar and K. Rustan M. Leino
		Formal Aspects of Computing, 7(6):683-703, March 1995.
	Constructing a program with exceptions		IPL
	K. Rustan M. Leino
		Information Processing Letters, 53(3):159-163, February 1995.
	A method for showing progress		FAC
	K. Rustan M. Leino
		Formal Aspects of Computing, 7(5):567-580, January 1995.

	A verifying compiler for a multi-threaded object-oriented language
	K. Rustan M. Leino and Wolfram Schulte
		To appear in the Marktoberdorf Summer School 2006 lecture notes.
	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..
	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.
	A logic of object-oriented programs
	Martin 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.

	Data abstraction and information hiding		SRC RR
	K. Rustan M. Leino and Greg Nelson
		Research Report 160, Compaq Systems Research Center, Palo Alto, CA, November 2000.
		Superseded by TOPLAS article, see above.
	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.
	A logic of object-oriented programs		SRC RR
	Martin Abadi and K. Rustan M. Leino
		Research Report 161, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, September 1998.
		Superseded by chapter in Zohar Manna's Festschrift, see above.
	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.

	Verification of equivalent-results methods		ESOP 2007
	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.
	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.
	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.
	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, 2007.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
		Superseded by SCP article, see above.
	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.
		Superseded by NJC article, see above.
	A logic of object-oriented programs		TAPSOFT '97
	Martin 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.
		Superseded by chapter in Zohar Manna's Festschrift, see above.
	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.

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

(other than older versions of the above)

	Automatic verification of textbook programs that use comprehensions		FTfJP 2007
	K. Rustan M. Leino and Rosemary Monahan
		In proceedings of 9th workshop on Formal Techniques for Java-like Programs (FTfJP 2007), July 2007.
	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.
	Verified Software: Theories, Tools, and Experiments, VSTTE 2006, Workshop proceedings		MSR TR
	K. Rustan M. Leino and Wolfram Schulte, editors
		Technical Report MSR-TR-2006-117, Microsoft Research, August 2006.
	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.
	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.
	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.
	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), 2005.
	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.
	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.
	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).
	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), 2003.
	An overview of JML tools and applications		FMICS 03
	Lilian Burdy, Yoonsik Cheon, David Cok, Michael D. Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll
		Presented at Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03), Trondheim, Norway, June 2003.  A previous version appeared as University of Nijmegen Dept. of Computer Science technical report NIII-R0309, March 2003.
		Superseded by STTT article, see above.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.
	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.

(other than conference and workshop presentations of papers above)

• Program verification using the Spec# programming system
  • With Rosemary Monahan.  Tutorial, ETAPS 2008, Budapest, Hungary (March 2007).
• Specifying and verifying software
  • Chalmers, Göteborg, Sweden (Nov 2007)
  • Invited talk, ASE 2007, Atlanta, GA (Nov 2007).
• Spec#
  • Invited talk, Øredev, Malmö, Sweden (Nov 2007).
• Designing a type system for BoogiePL 2
  • IFIP WG 2.3 meeting 47, Santa Fe, NM (Oct 2007).
• Designing verification conditions for software
  • Invited talk, CADE-21, Bremen, Germany (Jul 2007).
• Program verification via an intermediate language
  • Seminar, National University of Ireland, Maynooth, Maynooth, Ireland (Jun 2007).
• Verifying object-oriented software: Lessons and challenges
  • Invited talk, TACAS 2007, part of ETAPS in Braga, Portugal (Mar 2007).
• Reasoning about object structures in Spec#
  • UNSW, Sydney, Australia (Jan 2007).
  • INRIA + Microsoft lab, Paris, France (Nov 2006).
• Automatic verification of summations
  • IFIP WG 2.3 meeting 46, Sydney, Australia (Jan 2007).
• Going beyond a simple ownership system in Spec#
  • European Science Foundation workshop on Java program verification, Nijmegen, The Netherlands (Oct 2006).
• Object invariants in specification and verification
  • Invited talk, Brazilian Symposium on Formal Methods (SBMF 2006), Natal, Brazil (Sep 2006).
• Spec#
  • Microsoft Research Faculty Summit 2006, Redmond, WA (Jul 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, Bruges, Belgium (Apr 2006).
• Invariants on demand
  • Invited talk, 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), Koblenz, Germany (Sep 2005).
• Loop invariants on demand
  • IFIP WG 2.3 meeting, Niagara Falls, ON (Jun 2005).
• The Spec# programming system
  • Distinguished Lecture, Max-Planck Institute for Software Systems, Kaiserslautern, Germany (Mar 2006).
  • Seminar, Åbo Akademi University, Turku, Finland (Dec 2005).
  • Lunch seminar, Praxis High Integrity Systems, Bath, UK (Dec 2005).
  • Short presentation and demo, Verified Software: Theories, Tools, Experiments (VSTTE 2005), Zurich, Switzerland (Oct 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 at the Fourth International Workshop on Automated Verification of Infinite-State Systems (AVIS'05), Edinburgh, Scotland, UK (April 2005).
• Program verification and programming methodology.
  • Invited talk at the 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 at the first International Workshop on Abstract Interpretation of Object-Oriented Languages, Paris, France (January 2005).
• Challenges in increasing tool support for programming.
  • Invited talk at the first International Colloquium on Theoretical Aspects of Computing, Guiyang, Guizhou, China (September 2004).
• Spec#: Writing and checking contracts in a .NET language.
  • Keynote talk at .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 (Apr/May 2004).
• Toward enforceable contracts in .NET
  • Keynote talk at workshop on Construction and Analysis of Safe, Secure and Interoperable Smart devices (CASSIS 2004), Marseille, France (Mar 2004).
• Abstract interpretation for heap structures
  • IFIP WG 2.3 meeting, Philadelphia, PA (Jan 2004).
• Verifying invariants in object-oriented programs
  • Colloquium, Department of Computer Science, ETH Zurich, Switzerland (Nov 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 (Sep 2003).
• Static program checking, module by module
  • Invited tutorial, Prato workshop on Trusted Components, Prato, Italy (Jan 2003).
• A SAT characterization of boolean-program correctness.
  • IFIP WG 2.3 meeting, Biarritz, France (Mar 2003).
  • Department colloquium, Washington University in St. Louis, St. Louis, MO (Feb 2003).
  • IFIP WG 2.4 meeting, Schloss Dagstuhl, Germany (Nov 2002).
  • University of Eindhoven, Eindhoven, The Netherlands (Nov 2002).
• ESC/Java or Light-weight formal methods: from objects to components.  (On joint work with Cormac Flanagan, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.)
  • Invited talk, First international symposium on Formal Methods for Components and Objects (FMCO 2002), Leiden, The Netherlands (Nov 2002).
• Checking correctness properties of object-oriented programs.  5 lectures.
  • EEF Summer School on Specification, Refinement and Verification, Turku, Finland (Aug 2002).
• Modular checking and side effects.
  • IFIP WG 2.3 meeting, Turku, Finland (Aug 2002).
• Checking side effects in object-oriented programs.
  • Invited talk, Java Verification Workshop (JVW'02), Portland, OR (Jan 2001).
• ESC/Java: The Greatest Thing Since Sliced Bread.
  • Distinguished Lecturer Series, Computing and Information Sciences, Kansas State University, Manhattan, KS (Oct 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.  (On joint work with Cormac Flanagan, Rajeev Joshi, and Michael Y. Levin.)
  • 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).
  • Software verification tools summit, Compaq, Houston, TX (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, Santa Cruz, CA (January 2001).
• Program checking.  (On joint work with Cormac Flanagan, David L. Detlefs, Mark Lillibridge, Todd D. Millstein, Greg Nelson, James B. Saxe, and Raymie Stata.)
  • Invited talk at 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 at In Pursuit of Simplicity, a symposium honoring Edsger W. Dijkstra, UT Austin, Austin, TX (May 2000).
• Extended static checking for Java.  (On joint work with Cormac Flanagan, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata, and Yuan Yu.)
  • Automated Software Engineering Group seminar, NASA Ames, Mountain View, CA (Nov 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.  (On joint work with Cormac Flanagan, Rajeev Joshi, Mark Lillibridge, Todd D. Millstein, Greg Nelson, James B. Saxe, Raymie Stata, Caroline Tice, and Yuan Yu.)
  • IFIP WG 2.3 meeting, Longhorsley, England (April 2000).
• ESC/Java. (On joint work with Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata, and Cormac Flanagan.)
  • 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, Computing and Information Sciences, Kansas State University, Manhattan, KS (Oct 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, Bloomington, IN (June 1998).
• Extended static checking. (On joint work with David L. Detlefs, Greg Nelson, James B. Saxe, Raymie Stata, Cormac Flanagan, and Mark Lillibridge.)
  • Invited talk at PROCOMET'98, Shelter Island, NY (June 1998).
• A semantic approach to secure information flow. (On joint work with Rajeev Joshi.)
  • California Institute of Technology, Pasadena, CA (March 1998).
  • IFIP WG 2.3 meeting, Alsace, France (September 1997).
• Soundness and completeness considered harmful. (On joint work with Cormac Flanagan, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.)
  • SRI computer science seminar, Menlo Park, CA (May 1998).
• Object invariants in Java. (On joint work with Raymie Stata.)
  • IFIP WG 2.3 meeting, Alsace, France (September 1997).
• Generalized data abstraction. (On joint work with Greg Nelson.)
  • IFIP WG 2.3 meeting, Napa Valley, CA (January 1997).
• Extended static checking. (On joint work with David L. Detlefs, Greg Nelson, and James B. Saxe).
  • 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. (On joint work with Greg Nelson.)
  • Microsoft Research, Redmond, WA (January 1995).

• Member, IFIP Working Group 2.3 "Programming Methodology", 2000-present.  (Secretary, 2003-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.)

• 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), 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, at ICSE, Toronto, Canada (May 2001).
• Mathematics of Program Construction (MPC 2000), Ponte de Lima, Portugal, July 2000.
• Intercontinental Workshop on Aliasing in Object-Oriented Systems, in conjunction with ECOOP, Lisbon, Portugal, June 1999.
• Workshop on Program Analysis, Testing and Verification, at ICSE, University of Limerick, Ireland, June 2000.
• The Sixth International Workshop on Foundations of Object-Oriented Languages (FOOL 6), at POPL, San Antonio, TX, January 1999.

• Project evaluator, Research theme A: Symbolic systems, INRIA, 2006.
• Scientific advisory board, Mobius project, 2005-2007.
• Summer intern mentor, Microsoft Research:
  • 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.
• Project retreat external visitor, Open Software Quality project, UC Berkeley, May 2001.
• Habilitation thesis committee:
  • Claude Marché, University Paris 11, 2005.
• PhD thesis committee:
  • 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.
• Summer intern host, Compaq SRC:
  • Todd Millstein (University of Washington), 1999.
  • Rajeev Joshi (The University of Texas at Austin), 1997.
• 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.

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

• Boss Higher. 1997, 1999. Available from http://leino-online.com/games.

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

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

Acknowledgement: Ken Beckman made the videos in the second group above possible and lots of fun.

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

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

• Group Exercise Volunteer (step aerobics instructor), Bellevue Family YMCA, Bellevue, WA.  2004-present.
• 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 August 2007.