Arthur Azevedo de Amorim — Rochester Institute of Technology

Introduction to Rocq

Philippa Gardner — Imperial College London

Separation Logic and Compositional Symbolic Execution:
Verification and Bug Detection at Scale

Herman Geuvers — Radboud University Nijmegen

Introduction to Type Theory

Rustan Leino — Amazon Web Services

The Use and Anatomy of an Auto-Active Verifier

Plan for the lectures:

• Writing programs (contracts, invariants)
• Writing proofs (assertions, calculations, induction)
• Building a verifier (architecture, intermediate verification language)
• Language design: Changing the rules

Simon Peyton Jones — Epic Games

The Verse Language: Types, Semantics, and Verification

Jonathan Protzenko — Google Information Security

Linearity Rust Verification