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

Nov 12

Stochastic search continued. Estimation. Population-based approaches and evolutionary algorithms.

Readings:

1. Estimating the efficiency of backtrack programs
2. (Optional) Go with the winners
3. (Optional) Stochastic enumeration

Nov 19

Symbolic search and SAT solving. How to verify assertions by a powerful agent?

Readings:

1. SAT Solving
2. SATLution
3. (Optional) Quanta article

Nov 26

Autoformalization

Readings:

1. Specifications: The missing link to making the development of LLM systems an engineering discipline
2. Autoformalization with Large Language Models
3. A Neurosymbolic Approach to Natural Language Formalization and Verification

Dec 3

No Class. Work on reading list.

Readings:

See below for the next weeks.

Dec 10

``AI Scientist’’: Search in scientific discovery

Readings

1. AI-Scientist
2. AI-Scientist 2
3. Open ended scientific discovery via Bayesian surprise

Dec 17

AI for Systems Research

Readings

1. Barbarians at the gate
2. Metastable failures

Jan 07

AI for Math

Readings

1. AlphaProof Blog Post
2. AlphaProof paper
3. Mathematical exploration and discovery at scale

Jan 14

Agents. Cooperation, equilibria, persuasion.

Readings

1. ADAS
2. Program equilibria
3. Agree to disagree
4. Bayesian persuasion.

Jan 21

Jan 28

Student presentations

Feb 04

Student presentations