A selection of lectures and talks

K. Rustan M. Leino.

• Tools for software verification: an industrial perspective [PowerPoint] [PDF]
  Invited tutorial, LICS 2025, Singapore, June 2025.

• Reasoning about allocation [PowerPoint] [PDF]
  IFIP Working Group 2.3 meeting 69, Athens, Greece, May 2025.

• B3: a next-generation intermediate verification language [PowerPoint]
  PNW PLSE 2025, Seattle, WA, USA, May 2025.

• Dafny 2025 State of the Union Address [PowerPoint] [PDF]
  Keynote, Dafny Workshop 2025, Denver, CO, USA, January 2025.

• Using Dafny to write correct programs [PowerPoint] [PDF]
  TU Vienna, Vienna, Austria, October 2024.

• Writing proofs in Dafny [PowerPoint] [PDF]
  Invited tutorial, FMCAD 2024, Prague, The Czech Republic, October 2024.

• Induction in deductive reasoning [PowerPoint] [PDF]
  Marktoberdorf Summer School 2024, Herrsching, Germany, August 2024.

• Encoding partial functions into a total logic [PowerPoint] [PDF]
  IFIP Working Group 2.3 meeting 68, Princeton, NJ, USA, May 2024.

• The life of a scientist: dream, build, learn, explain [PowerPoint] [PDF]
  Invited talk, PhD Symposium, iFM 2023, Leiden, The Netherlands, November 2023.

• Industrial experience with a verification-aware programming language [PowerPoint] [PDF]
  Keynote, Integrated Formal Methods (iFM 2023), Leiden, The Netherlands, November 2023.

• Tracked regions [HTML]
  IFIP Working Group 2.3 meeting 67, Trento, Italy, October 2023.

• State of state in Dafny [HTML]
  Keynote, Formal Techniques for Java-like Programs workshop (FTfJP 2023), Seattle, WA, USA, July 2023.

• What’s new in Dafny? And what is Dafny, anyway? [HTML]
  Invited tutorial, PLDI 2023, Orlando, FL, USA, June 2023.

• Verified programs and proofs in Dafny [PowerPoint]
  Summer School on Formal Techniques, Atherton, CA, USA, May 2017.