New edition of this course is SAV 2012.

Week 01, February 21

• Lecture 01 - Introduction to Verification. Monday, February 21 at 14:15, INR 219
• Exercise 01 - Hands-on specification and verification in Spec#. Tuesday, February 22 at 16:15, INM 10
• Lab 01 - Introductory Lecture about Synthesis. Background on sets and relations, Friday, February 25, INR 219
• Homework 01

Week 02, February 28

• Lecture 02 - Lecture on relational semantics, Monday, February 28
• Exercise 02 - First-order 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 - One-Point 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
• Lecture 10
  • 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 First-Order Logic

Friday, June 10: Project Reports Due in Moodle (5 pages, 2 column)

• Course Schedule
• Projects are due on June 10th
• Previous courses: SAV 2010, SAR 2010, SAV 2009, SAV 2008
• Course Staff:
  • Viktor Kuncak
  • Eva Darulova
  • Giuliano Losa

• 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