Lectures and talks

• Invited lectures and conference talks
• University and summer school lectures

[See also my papers page.]

Invited lectures and conference talks

• Dafny: An automatic program verifier for functional correctness.  Paper talk at LPAR-16, Dakar, Senegal, April 2010.
• The Dafny program verifier.  Seminar, Victoria University of Wellington, Wellington, New Zealand, April 2010.
• Contracts, tools, verification.  Keynote lecture, ASWEC 2010, Auckland, New Zealand, April 2010.
• Deadlock-free channels and locks.  Paper talk at ESOP 2010, Paphos, Cyprus, March 2010.
• Verifying Concurrent Programs with Chalice.  Keynote lecture, VMCAI 2010, Madrid, Spain, January 2010.
• Fun with code, tests, and verification.  "Cool technology" talk in CS 141, Caltech, November 2009.
• Understanding program verification.  Keynote lecture, PROLE 2009, San Sebastián, Spain, September 2009.
• Verifying concurrent object-oriented programs.  Seminar, EPFL, Lausanne, Switzerland, September 2009.
• Comparing heap models: Ownership, Dynamic Frames, Permissions.  Typing, Analysis and Verification of Heap-Manipulating Programs seminar, Dagstuhl, Germany, July 2009.
• Dynamic-frame specifications in Dafny.  JML seminar, Dagstuhl, Germany.  July 2009.
• Locks, channels, deadlock freedom, progress.  IFIP WG 2.3 meeting, MIT, June 2009.
• Correct Concurrency with Chalice.  MIT seminar, June 2009.
• Reasoning about Comprehensions with First-Order SMT Solvers.  Paper talk at SAC 2009, Honolulu, HI, USA, March 2009.
• Correct Concurrency with Chalice.  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, Venice, Italy, December 2008.
•  Specification techniques for verifying object-oriented software.  Seminar, U. 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.
•  Flexible immutability with frozen objects.  Paper talk at VSTTE 2008, Toronto, ON, Canada.
• Program Verification Using the Spec# Programming System.  Tutorial at ETAPS 2008, Budapest, Hungary, March 2008.
• Class-local object invariants.  Paper talk at ISEC 2008, Hyderabad, India.
• Specifying and verifying software.  CS Seminar, Chalmers, Göteborg, Sweden, November 2007.
• Spec#.  Invited talk at Øredev, Malmö, Sweden, November 2007.
• Specifying and verifying software.  Keynote talk at ASE 2007, Atlanta, GA, November 2007.
• Designing a type system for BoogiePL 2.  Presented at IFIP WG 2.3 meeting, Santa Fe, NM, October 2007.
• Designing verification conditions for software.  Invited talk at CADE-21, Bremen, Germany, July 2007.
• Program verification via an intermediate language.  Talk at NUI Maynooth, Maynooth, Ireland, June 2007.
• Verifying object-oriented software: Lessons and challenges.  Invited talk at TACAS 2007, ETAPS, Braga, Portugal, March 2007.
• Using history invariants to verify observers.  Presented at ESOP 2007, Braga, Portugal, March 2007.  Joint work with Wolfram Schulte.
• Reasoning about object structures in Spec#.  Talk at UNSW, Sydney, Australia, January 2007.
• Automatic verification of summations.  Presented at IFIP WG 2.3 meeting, Sydney, Australia, January 2007.
• Reasoning about object structures in Spec#.  Talk at INRIA + Microsoft lab, Paris, France, November 2006.
• Going beyond a simple ownership system in Spec#, ESF workshop on Java program verification, Nijmegen, NL, October 2006.
• Object invariants in specification and verification.  Invited talk, Brazilian Symposium on Formal Methods (SBMF 2006), Natal, Brazil, September 2006.
• Spec#, lecture at the Microsoft Research Faculty Summit, 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.
• The Spec# programming system.  Distinguished lecture, Max-Planck Institute for Software Systems, Kaiserslautern, Germany, March 2006.
• The Spec# programming system, lunch seminar, Praxis High Integrity Systems, Bath, UK, December 2005.
• The Spec# programming system (demo, call for methodology, infrastructure reuse).  Verified Software: Theories, Tools, Experiments working conference, Zurich, Switzerland, October 2005.
• Invariants on demand.  Invited talk at SEFM 2005, Koblenz, Germany, September 2005.  Joint work with Francesco Logozzo.
• The Spec# programming system.  Distinguished lecture, McMaster University, Hamilton, ON, May 2005.  Also: Colloquium, U. of Toronto, Toronto, ON, May 2005.
• Advanced programming tools at Microsoft.  Distinguished lecture, York University, Toronto, ON, May 2005.
• A two-tier approach for supporting quantifiers in a lazily proof-explicating theorem prover.  Presented at TACAS 2005, Edinburgh, Scotland, UK, April 2005.  Joint work with Madan Musuvathi and Xinming Ou.
• Demand-driven inference of loop invariants in a theorem prover.  Invited talk, AVIS 2005, Edinburgh, Scotland, UK, April 2005.  Joint work with Francesco Logozzo.
• Program verification and programming methodology.  Invited talk, ASM 2005, Paris, France, March 2005.
• Programming methodology.  Panel discussion, Verification Grand Challenge workshop, Menlo Park, CA, February 2005.
• Writing specifications for object-oriented programs.  Invited talk, AIOOL 2005, Paris, France, January 2005.
• Challenges in increasing tool support for programming.  Invited talk, ICTAC 2004, Guiyang, Guizhou, China, September 2004.
• On bounded model checking, abstract interpretation, interpolants, and induction. [PDF]  Presented at IFIP WG 2.3 meeting, Prato, Italy, September 2004.
• Spec#: Writing and checking contracts in a .NET language.  Keynote talk at .NET Technologies 2004, June 2004.
• Toward enforceable contracts in .NET.  Keynote talk at CASSIS, March 2004.
• Verifying invariants in object-oriented programs.  Colloquium, ETH Zurich, November 2003.
• Verification of object-oriented programs with invariants.  Presented at Formal Techniques for Java-like Programs (FTfJP), July 2003.
• Using data groups to specify and check side effects, presented at PLDI 2002.  Joint work with Arnd Poetzsch-Heffter and Yunhong Zhou.
• Extended Static Checking for Java, presented at PLDI 2002.  Joint work with Cormac Flanagan, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.
• Extended Static Checking for Modula-3, presented at CC 1998 (part of ETAPS 1998).  Tool paper with Greg Nelson; also joint work with David L. Detlefs and James B. Saxe.

University and summer school lectures

In September 2009, I lectured at FOSAD in Bertinoro, Italy:

• Lecture 0, A Foundation for Verifying Concurrent Programs
• Lecture 1, A Foundation for Verifying Concurrent Programs
• Chalice examples used in demos

In August 2008, I lectured at the International Summer School Marktoberdorf, Germany:

• Lecture 0, Specification and Verification of Object-Oriented Software
• Lecture 1, Specification and Verification of Object-Oriented Software
• Lecture 2, Specification and Verification of Object-Oriented Software
• Lecture 3, Specification and Verification of Object-Oriented Software
• Lecture 4, Specification and Verification of Object-Oriented Software

In July 2008, I lectured at the Summer School on Logic and Theorem-Proving in Programming Languages in Eugene, OR:

• Lecture 0, Specification and Verification of Programs with Pointers
• Lecture 1, Specification and Verification of Programs with Pointers

In May 2006, I gave a guest lecture on

• Building a program verifier

in Shaz Qadeer's CSE 599f, Formal Verification of Computer Systems class at UW.

In April/May 2004, I gave some guest lectures on Hoare-style program verification in Rob DeLine's CSE 503, Software Engineering course at UW.  Here are the PowerPoint slides from those lectures:

• Lecture 0:  Hoare logic and weakest preconditions.
• Lecture 1:  Proving programs with loops.
• Lecture 2:  Procedure specifications and tool support.

In September 2003, I lectured on Technologies for finding errors in object-oriented software at the United Nations University IIST and IFIP WG 2.3 Summer School on Formal Models of Software at École Polytechnique de Tunisie (EPT) in Tunis, Tunisia.  Here are the PowerPoint slides and one-sentence descriptions of the 4 lectures:

• Lecture 0: Motivation: Overview and demonstration of ESC/Java.
• Lecture 1: Semantics of procedural languages.
• Lecture 2: Semantics of object-oriented programming languages.
• Lecture 3: Programming methodology for object invariants and modifications of state.

There is also a list of selected bibliographic references.

In August 2002, I lectured on Checking correctness properties of object-oriented programs at the EEF Summer School on Specification, Refinement and Verification in Turku, Finland.  Here are the PowerPoint slides and one-sentence descriptions of the 5 lectures:

• Lecture 0: Motivation: Overview and demonstration of ESC/Java.
• Lecture 1: Semantics of procedural languages.
• Lecture 2: Semantics of object-oriented programming languages.
• Lecture 3: Use of abstraction in specifications.
• Lecture 4: Open problems in programming methodology.