Software Verification in Lean was a one-day open workshop dedicated to the formal verification of software using the Lean 4 theorem prover. The workshop brought together researchers and practitioners to share recent advances, practical techniques, and ongoing challenges in building verified software.
Schedule
9:00-10:00 — Max Tegmark and BAIF. Open tools and standards for scaling software verification (slides).
10:00–11:00 — Leo de Moura. Scalable Software Verification in Lean 4 (slides).
11:00–11:30 — Coffee break
11:30–12:30 — Son Ho. Co-development of code and proofs for SymCrypt
12:30–14:00 — Lunch break
14:00–15:00 — Derek Sorensen. Correct and Computable Specifications in Lean (slides).
15:00–15:30 — Coffee break
15:30–16:30 — Karthikeyan Bhargavan. Verifying Cryptographic Applications: Challenges and Opportunities.
Organizing Committee
Ashley Blacquiere (Lean FRO)
Oliver Butterley (BAIF)
Alessandro D'Angelo (BAIF)
Aymeric Fromherz (INRIA)
Venue
INRIA Paris, 48 rue Barrault, 75013 Paris, France