Some papers linked so far:

• A Methodology for Modular Termination Verification.  [PDF]
  K. Rustan M. Leino.
  Andreas Podelski Festschrift, Springer LNCS 14765, 2026.
• Formally verified cloud-scale authorization.  [link] [PDF] [video]
  Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Samuel Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clement Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas Wagner, Michael Whalen, Remy Willems, Tongtong Xiang, Taejoon Byun, Joshua M. Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, and Yongwei Yuan
  ICSE 2025.
• Free Facts: An alternative to inefficient axioms in Dafny.  [PDF]
  Tabea Bordis and K. Rustan M. Leino.
  FM 2024.
• Centuries and decades.  [HTML]
  K. Rustan M. Leino.
• Specifying the boundary between unverified and verified code.  [PDF]
  David R. Cok and K. Rustan M. Leino.
  Reiner Hähnle Symposium, 2022.
• Dafny Power User: Automatic Induction.  [HTML]
  K. Rustan M. Leino.
  KRML 269, 2019.
• Dafny Power User: Short-Circuit Operators.  [HTML]
  K. Rustan M. Leino.
  KRML 268, 2019.
• Dafny Power User: Comprehensions.  [HTML]
  K. Rustan M. Leino.
  KRML 267, 2019.
• Dafny Power User: Statement versus Expression Syntax.  [HTML]
  K. Rustan M. Leino.
  KRML 266, 2019.
• Dafny Power User: Calling Lemmas Automatically.  [HTML]
  K. Rustan M. Leino.
  KRML 265, 2019.
• Modular Verification Scopes via Export Sets and Translucent Exports.  [PDF]
  K. Rustan M. Leino and Daniel Matichuk.
  Festschrift for Arnd Poetzsch-Heffter, 2018.
• Accessible Software Verification with Dafny.  [PDF]
  K. Rustan M. Leino.
  IEEE Software 34(6): 94-97, 2017.
• Modeling Concurrency in Dafny.  [PDF]
  K. Rustan M. Leino.
  SETSS 2017.
• Trigger Selection Strategies to Stabilize Program Verifiers.  [PDF]
  K. Rustan M. Leino and Clément Pit-Claudel.
  CAV 2016.
• Well-founded Functions and Extreme Predicates in Dafny: A Tutorial.  [PDF]
  K. Rustan M. Leino.
  IWIL 2015.
• Compiling Hilbert's epsilon operator.  [PDF]
  K. Rustan M. Leino.
  LPAR-20 2015.
• Programming Language Features for Refinement.  [PDF]
  Jason Koenig and K. Rustan M. Leino.
  EPTCS, 2016. (Post-workshop proceedings of REFINE 2015.)
• Automatic Verification of Dafny Programs with Traits [PDF]
  Reza Ahmadi, K. Rustan M. Leino, and Jyrki Nummenmaa.
  Formal Techniques for Java-like Programs 2015.
• Fine-grained Caching of Verification Results.  [PDF]
  K. Rustan M. Leino and Valentin Wüstholz.
  CAV 2015.
• Types in Dafny.  [HTML]
  K. Rustan M. Leino.
  February 2015.
• Computing with an SMT solver.  [PDF]
  Nada Amin, K. Rustan M. Leino, and Tiark Rompf.
  TAP 2014.
• The Dafny Integrated Development Environment.  [PDF]
  K. Rustan M. Leino and Valentin Wüstholz.
  Formal-IDE 2014.
• Automating Theorem Proving with SMT [PDF]
  K. Rustan M. Leino.
  ITP 2013.
• Developing Verified Programs with Dafny [PDF]
  K. Rustan M. Leino.
  Tutorial notes, ICSE 2013.
• Verified Calculations [PDF]
  K. Rustan M. Leino and Nadia Polikarpova.
  VSTTE 2013.
• Co-induction simply [PDF]
  K. Rustan M. Leino and Michał Moskal.
  FM 2014.
• Abstract Read Permissions: Fractional Permissions without the Fractions [PDF]
  Stefan Heule, K. Rustan M. Leino, Peter Müller, and Alexander J. Summers.
  VMCAI 2013.
• Behavioral Interface Specification Languages [PDF]
  John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson.
  ACM Computing Surveys 2012.
• Using Dafny, an Automatic Program Verifier [PDF]
  Luke Herbert, K. Rustan M. Leino, and Jose Quaresma.
  LASER International Summer School 2011, lecture notes.
• Program Extrapolation with Jennisys [PDF]
  K. Rustan M. Leino and Aleksandar Milicevic.
  OOPSLA 2012.
• Automating Induction with an SMT Solver [PDF]
  K. Rustan M. Leino.
  VMCAI 2012
• Stepwise Refinement of Heap-Manipulating Code in Chalice [PDF]
  K. Rustan M. Leino and Kuat Yessenov.
  In Carroll Morgan's Festschrift, 2012.
• Tools and Behavioral Abstraction: A Direction for Software Engineering [PDF]
  K. Rustan M. Leino.
  In The Future of Software Engineering, 2010.
• The Boogie Verification Debugger [PDF]
  Claire Le Gouess, K. Rustan M. Leino, and Michał Moskal.
  SEFM 2011.
• VACID-0: Verification of Ample Correctness of Invariants of Data-structures, Edition 0 [PDF]
  K. Rustan M. Leino and Michał Moskal.
  Tools & Experiments Workshop at VSTTE 2010, 2010.
• Specification and Verification: The Spec# Experience [CACM] [CACM PDF] [PDF]
  Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Mülller, Wolfram Schulte, and Herman Venter.
  CACM 54(6): 81-91, 2011.
• Getting Started with Dafny: A Guide [PDF]
  Jason Koenig and K. Rustan M. Leino.
  Marktoberdorf International Summer School 2011, lecture notes.
• Usable Auto-Active Verification.  [PDF]
  K. Rustan M. Leino and Michał Moskal.
  UV 2010, 2010.
• To Goto Where No Statement Has Gone Before [PDF]
  Mike Barnett and K. Rustan M. Leino.
  VSTTE 2010.
• Dafny: An Automatic Program Verifier for Functional Correctness [PDF]
  K. Rustan M. Leino.
  LPAR-16, April 2010.
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding [PDF]
  K. Rustan M. Leino and Philipp Rümmer.
  TACAS 2010.
• Deadlock-free Channels and Locks [PDF]
  K. Rustan M. Leino, Peter Müller, and Jan Smans.
  ESOP 2010.
• Verification of concurrent programs with Chalice [PDF]
  K. Rustan M. Leino, Peter Müller, and Jan Smans.
  In Foundations of Security Analysis and Design V, 2007/2008/2009 Tutorial Lectures. LNCS 5705, Springer, 2009.
• Position Statement: Ceaselessly-Analyzing Development Environments, One Direction For the Next 40 Years of Software Engineering [PDF]
  K. Rustan M. Leino.
  COMPSAC 2010.
  
• Reasoning about Comprehensions with First-Order SMT Solvers [PDF]
  K. Rustan M. Leino and Rosemary Monahan.
  SAC 2009.
  
• A basis for verifying multi-threaded programs [PDF]
  K. Rustan M. Leino and Peter Müller.
  ESOP 2009.
• Specification and verification of object-oriented software [PDF]
  K. Rustan M. Leino.
  Marktoberdorf International Summer School 2008, lecture notes.
• Using the Spec# language, methodology, and tools to write bug-free programs [PDF]
  K. Rustan M. Leino and Peter Mülller
  LASER Summer School 2007/2008, LNCS 6029. 2009.
• It's doomed; We can prove it! [PDF]
  Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, and Thomas Wies
  Formal Methods 2009, LNCS 5850, pages 338-353. 2009.
• Verification of equivalent-results methods [PDF]
  K. Rustan M. Leino and Peter Müller.
  ESOP 2008.
• Using History Invariants to Verify Observers. [PDF]
  K. Rustan M. Leino and Wolfram Schulte.
  ESOP 2007.
• Practical reasoning about invocations and implementations of pure methods. [PDF]
  Adam Darvas and K. Rustan M. Leino.
  FASE 2007.
• Specification and verification challenges for sequential object-oriented programs. [PDF]
  Gary T. Leavens, K. Rustan M. Leino, and Peter Müller.
  TR #06-14b, KRML 161, May 2006, revised August 2006, corrected July 2008.
• A verifying compiler for a multi-threaded object-oriented language. [PDF]
  K. Rustan M. Leino and Wolfram Schulte.
  Marktoberdorf International Summer School 2006, lecture notes.
• Loop invariants on demand. [PDF]
  K. Rustan M. Leino and Francesco Logozzo.
  APLAS 2005.
• Safe concurrency for aggregate objects with invariants. [PDF]
  Bart Jacobs, K. Rustan M. Leino, Frank Piessens, and Wolfram Schulte.
  SEFM 2005.
• Weakest-Precondition of Unstructured Programs [PDF]
  Mike Barnett and K. Rustan M. Leino.
  PASTE 2005.
• Boogie: a modular reusable verifier for object-oriented programs [PDF]
  Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.
  FMCO'05: Proceedings of the 4th international conference on Formal Methods for Components and Objects, pages 364-387, 2005.
• Efficient weakest preconditions [PDF]
  K. Rustan M. Leino.
  Information Processing Letters, 93(6), 2005.
• Exception safety for C# [PDF]
  K. Rustan M. Leino and Wolfram Schulte.
  SEFM 2004.
• Object invariants in dynamic contexts [PDF]
  K. Rustan M. Leino and Peter Mäller.
  ECOOP 2004.
• Verification of object-oriented programs with invariants [PDF]
  Mike Barnett, Robert DeLine, Manuel Fähndrich, K. Rustan M. Leino, Wolfram Schulte.
  JOT 3(6), 2004.
• Generating error traces from verification-condition counterexamples [PDF]
  K. Rustan M. Leino, Todd Millstein, and James B. Saxe.
  SCP 55(1-3), 2004.
• Finding stale-value errors in concurrent programs [PDF]
  Michael Burrows and K. Rustan M. Leino.
  Concurrency and Computation: Practice and Experience 16(12), 2004.
• Heap monotonic typestate [PDF]
  Manuel Fähndrich and K. Rustan M. Leino.
  International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO), 2003.
• Declaring and checking non-null types in an object-oriented language.  [PDF]
  Manuel Fähndrich and K. Rustan M. Leino.
  OOPSLA 2003, ACM SIGPLAN Notices, 38(11), 302-312, October 2003.
• Data Abstraction and Information Hiding.  [PDF]
  K. Rustan M. Leino and Greg Nelson.
  ACM TOPLAS, 24(5), 491-553, September 2002.
• Extended Static Checking for Java.  [ACM Digital Library]
  Cormac Flanagan and K. Rustan M. Leino and Mark Lillibridge and Greg Nelson and James B. Saxe and Raymie Stata.
  PLDI 2002, 234-245, ACM, 2002.
• Extended Static Checking: A Ten-Year Perspective.  [PDF]
  K. Rustan M. Leino.
  Informatics --- 10 years back, 10 years ahead, LNCS 2000, 157-175, 2001.
• Efficient Annotation Inference for an Extended Static Checker.  [PDF]
  Cormac Flanagan, K. Rustan M. Leino, and Michael Y. Levin.
  Unpublished, Compaq SRC, 2001.
• Houdini, an Annotation Assistant for ESC/Java.  [PDF]
  Cormac Flanagan and K. Rustan M. Leino.
  FME 2001, LNCS 2021, 500-517, 2001.
• Real Estate of Names.  [PDF]
  K. Rustan M. Leino.
  Information Processing Letters, 77(2-4):169-171, February 2001.
• Annotation Inference for Modular Checkers.  [PDF]
  Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino.
  Information Processing Letters, 77(2-4):97-108, February 2001.
• ESC/Java User's Manual [PDF]
  K. Rustan M. Leino, Greg Nelson, and James B. Saxe.
  Compare SRC Technical Note 2000-002, October 2000.
• Extended static checking [PDF]
  David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe.
  DEC SRC Research Report 159, December 1998.
• Data abstraction and information hiding [PDF]
  K. Rustan M. Leino and Greg Nelson.
  DEC SRC Research Report 160, November 2000.
• Data groups: Specifying the modification of extended state.  [PDF]
  K. Rustan M. Leino.
  OOPSLA 1998.
• Wrestling with rep exposure.  [PDF] (also, [SRC Report 156])
  David L. Detlefs, K. Rustan M. Leino, and Greg Nelson.
  DEC SRC Research Report 156, July 1998.
• Virginity: A contribution to the specification of object-oriented software.  [PDF]
  K. Rustan M. Leino and Raymie Stata.
  Information Processing Letters, 70(2):99-105, April 1999.
• Computing Permutation Encodings.  [PDF]
  K. Rustan M. Leino.
  Formal Aspects of Computing, 11(1):56-74, 1999.
• Joining Specification Statements.  [PDF]
  K. Rustan M. Leino and Rajit Manohar.
  Theoretical Computer Science, 216(1-2):375-394, 1999.
• Ecstatic: An object-oriented programming language with an axiomatic semantics.  [PDF]
  K. Rustan M. Leino.
  Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages, January 1997.
• ESCJ notes
• Toward Reliable Modular Programs.  [PDF]
  K. Rustan M. Leino.
  Caltech PhD thesis, 1995.

Some talks linked so far:

• [Link to talks]