Synthesis, Analysis, and Verification (SAV 2011)
New edition of this course is SAV 2012.
Course Material
Week 01, February 21
 Lecture 01  Introduction to Verification. Monday, February 21 at 14:15, INR 219
 Exercise 01  Handson specification and verification in Spec#. Tuesday, February 22 at 16:15, INM 10
Week 02, February 28
 Lecture 02  Lecture on relational semantics, Monday, February 28
 Exercise 02  Firstorder logic and relations, Tuesday, March 1
 Lab 02  Labs on doing proofs using the Isabelle interactive proof assistant
 Homework 02  Expressions built from relations. Isabelle
Week 03, March 07
 Lecture 03  Hoare logic. Building formulas from programs
 Exercise 03  More Hoare Logic. Construction of formulas
 Lab 03  Exercises and a 1/2 lecture on Strongest Postconditions
 Homework 03  Hoare logic
Week 04, March 14
 Lecture 04  Weakest Preconditions and Hoare Logic
 Exercise 04  OnePoint Rule
 Lab 04  Modeling Data Structures
 Homework 04  Arrays and VCG for a simple programming language
Week 05, March 21
 Lecture 05  Homework discussion and exercises
 Exercise 05  Modeling Arrays and Fields
 Lab 05  Models of Dynamic Memory Allocation. Definition of WS1S
Week 06, March 28
 Lecture 06  preparation for the quiz
 Exercise 06  Quiz from 16:00 until 19:00 (not open book)
 Labs 06  Lecture on Predicate Abstraction for Invariant Inference
Week 07, April 4
 Lecture 07  Lecture and Demo of Verification of Functional Programs in Scala
 Exercise 07  Mini Project Discussions. Quantifier Elimination
 Labs 07  More Quantifier Elimination
Week 08, April 11
 Lecture 08  BAPA and WS1S
 Exercise 08  WS1S and Tree Automata
 Labs 08  Quiz discussion and exercises
Week 09, April 18
 Lecture 09: Abstract Interpretation Idea

 Demonstration of Simplex Solver for Linear Equations
 Discussion of Projects
 No Labs 10, holiday, see school calendar
Week 10, April 25
 Still school holidays, see school calendar
Week 11, May 2
 Lecture 11: Remaining project descriptions. Exercises with lattices
 Exercise 11  Fixpoint theorems. Galois connection. Transition system.
 Labs 11  Abstract interpretation Framework
Week 12, May 9
 Lecture 12: Combining Galois Connections. Predicate Abstraction Demo
 Exercise 12: Collecting Semantics and its Abstract Interpretation. Fixed point and Prefix Point Formulation through example
 Labs 12: Abstract interepretation through example
Week 13, May 16
 Monday: Phantm and Insane tools
 Tuesday: Quiz gymnastics through monotonic functions on sets. Remarks on predicate abstraction
 Friday: Quiz
Week 14, May 23
 Lecture 14: Chaotic Iteration. Widening and Narrowing
 Exercise 14: Procedures
 Labs 14: Quiz Discussions
Week 15, May 30
 Lecture 15: Automating FirstOrder Logic
Friday, June 10: Project Reports Due in Moodle (5 pages, 2 column)
General Information
 Projects are due on June 10th
 Course Staff:
Announcements
February 17, 2011
 the first lecture will be on Monday, February 21st.
 in subsequent weeks, lecture, exercise, and lab slots are interchangeable, and will be announced the week before
 for all further announcements see http://moodle.epfl.ch forum