Calendar

Introduction to Software Verification

Oct 22
Introduction to software verification as search.

Readings:

  1. The Bitter Lesson
  2. Mathematical discoveries from program search with large language models (FunSearch)
  3. AlphaEvolve

Assignment

Download OpenEvolve and go through its tutorial.

Oct 29
The internals of an enumerative checker for Java. [slides]

Readings:

  1. The Spin Model Checker
  2. Model Checking for Programming Languages using Verisoft

Assignment

Download JMC and go through its tutorial.

Nov 5
Heuristics for enumerative search. Randomization.

Readings:

  1. Stochastic Local Search Algorithms: An Overview

Symbolic Techniques

Nov 13
Symbolic analysis of programs: reductions to logic. Inductive invariants. Abstraction.
Nov 20
Interpolation and SAT-based Model Checking- Mcmillan’03.
Nov 27
IC3.