Taught in Spring 2008 by Viktor Kuncak and Ruzica Piskac from the LARA group.

• later edition: Software Analysis and Verification 2009

General Information

Licence and Copyright

Project suggestions (acess only for class members)

Projects completed by students:

• Ersoy Bayramoglu: Verification of Equals Methods in Java Programs
• Pierre-Evariste Dagand: Model Checking Opis
• Sebastian Gfeller: Combining Jahob and STP to Generate Test Cases
• Thomas Hofer: Solving Satisfiable Constraints over Finite Domains
• Thibaud Hottelier: Counterexample Analysis in Valigator
• David Joaquim: SAT Solver
• Giuliano Losa: Simple constant propagation for the simple programming language
• Stephane Rabie: Term Algebra Quantifier Elimination
• Damien Zufferey: Static Analysis on a Functional Subset of Scala

• Lecture 01: General Information, Motivation, Demos, Background
• Lecture 02: More Background
  • Exercises 01: Relations, Aunt Agatha, SPASS, formDecider, FOL Formulas, FOL is undecidable
  • Homework01

• Lecture 03: Program Semantics using Relations; Hoare Logic
• Lecture 04: Generating Verification Conditions
  • Exercises 02: Homework analysis, Proving properties of wp, sp
  • Homework02

• Lecture 05: More on Verification Condition Generation
• Lecture 06: Propositional Logic Formally
  • Exercises 03
  • Homework03

• Lecture 07: Propositional Proofs and Boolean Constraint Propagation
• Lecture 08: SAT Solvers and Model Finders
  • Exercises 04
  • Homework04

• Lecture 09: First-Order Logic Formally
• Lecture 10: Herbrand Theorem
  • Exercises 05
  • Homework05

• Lecture 11: Resolution, Equality
• Lecture 12: Equality, Decidable FOL Classes
  • Exercise 06
  • Homework06 (an alternative April 1st Version will also be accepted)

• Lecture 13: References, allocation, procedures
• Lecture 14: Reasoning with procedures. Quantifier Elimination Basics
  • Exercise 07
  • Homework07

• Lecture 15: QE for Presburger Arithmetic and Beyond
• Lecture 16: More QE. Some quantifier-free fragments
  • Exercise 08
  • Homework08
• Lecture 17: Congruence Closure
• Lecture 18: Combining Decision Procedures
  • Exercises 09
  • Homework09

• Lecture 19: Lattices and Fixpoints
  • Exercises10
  • Homework10

• Lecture 20: Abstract Interpretation
• Lecture 21: Predicate abstraction
  • Exercises11
  • Homework11

• Lecture 22: Logic and Automata: Deciding Presburger Arithmetic
• Lecture 23: Logic and Automata: Deciding MSOL over Strings and Trees
  • Exercies12
  • Homework12

• Lecture 24: Iteration, Range, Formulas, Constraints, Aliasing
• Lecture 25: Set Constraints, Shape, Interprocedural Analysis
  • Exercises13
  • Homework13

• Lecture 26: Higher-Order Logic and Interactive Provers

• Project presentations: Thursday, May 29th, 12:00-until we are done
  • Project write-up and source code are due on Friday, June 6, following the EPFL Academic Calendar

Here are last year's lectures.