Techniques for Program Verification

We are back! 🎉

In this session, George Zakhour, a PhD student at the Programming Group at the University of St.Gallen, will present "Techniques for Program Verification", focusing particularly on e-graphs.

E-graphs are at the heart of SMT solvers, a cornerstone of automated reasoning that powers applications from program verification to automated theorem proving. They are used for efficiently maintaining equalities and equivalence relations. Originally introduced in Greg Nelson's seminal 1980 PhD thesis, they gained widespread popularity for compiler optimization, program synthesis, and software testing thanks to the egg library (POPL' 21). In this talk, we will revisit Nelson's thesis, implement an e-graph live from scratch, and put it to work.

Why care?

• For verification enthusiasts: the e-graph is the congruence closure that propagates equalities from one theory to all the others. They allow you to build a large theory compositionally from smaller ones.
• For type system enthusiasts: e-graphs are the solvers of type inference constraints.
• For compiler enthusiasts: e-graphs eliminate phase ordering by searching many equivalent program optimizations at once.

The talk will be 45–60 minutes, followed by discussion, Q&A, and snacks. No prior background in SMTs is required; basic familiarity with compilers and formal methods will help.