Next edition: Synthesis, Analysis, and Verification 2011

Course Information

• Course in the Catalog
• 2009 Edition
• 2008 Edition

Moodle Page for Homework Submission

Week 01, February 22

• Lecture 01
• Exercises 01 in INM10
• Homework 01
• Some relevant easy reading, from CACM:
  • A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World
  • Retrospective: An Axiomatic Basis for Computer Programming
  • Model Checking: Algorithmic Verification and Debugging
  • Software Model Checking Takes Off
  • Formal Verification of a Realistic Compiler
  • seL4: Formal Verification of an Operating-System Kernel
    • Learning To Do Program Verification - a foreword by K. Rustan M. Leino

Week 02, March 01

• Exercises 02
• Lecture 02
• Talk Model Checking High level Petri Nets in room BC 355

Week 03, March 08

• Lecture 03
• Lecture 03a
• Exercises
• SAT solver competition

Week 04, March 15

• Monday: Exercises: first order logic, models
• Tuesday, 16:15: QUIZ
• Friday: Lecture 04

Week 05, March 22

• Monday: Quiz Solution Discussion. First project discussions.
• Tuesday 16:15: talk by Manuel Fähndrich (Microsoft Research)
• Labs 05
• Homework 02

Week 06, March 29

• Monday: Lecture 06
• Talk by Ranjit Jhala
• Tuesday 12:30 talk by Prof. Peter Mueller (EHTZ)
• Exercises 06
• Homework 03
• Invariants Space

Week 07, April 5 - Spring Break

Week 08, April 12

• Monday: Lecture 07: Abstract Interpretation
• Tuesday: talk by Alain Finkel (ENS Cachan)
• Friday: Lecture 08: Chaotic Iteration and Termination of Analysis

Week 09, April 19

• Monday 14:15: Lecture 09
• Tuesday 16:15: Lecture 10
• Friday
  • 10:30 Ciera Jaspan: Proper Plugin Protocols
  • 11:30 Exercises 09

Week 10, April 25

• Monday 14:15: Lecture 11, slides
• Tuesday, 16:15 talk by David Monniaux (VERIMAG, Grenoble),
  

→ see the paper Automatic modular abstractions for linear constraints in POPL 2009

• Wednesday, 18:00 Exercises 10
• Friday, 10:00 QUIZ

Week 11, May 3

• Monday 14:15: Lecture 12
• Tuesday, 16:15: Exercises
• Friday - no scheduled class; work on the project independently

Week 12, May 10

• Monday 14:15 Lecture 13: Modeling and Proving Properties about Sets and Data Structures
• Tuesday 16:15 Lecture 14: Reasoning about Reachability and Introduction to WS1S

Week 13, May 17

• Monday 14:15 Lecture 15: Decision Procedure for WS1S
• Tuesday 16:15: Individual work
• Friday 10:00 Lecture 16: Using WS1S. Notion of WS2S

Week 14, May 25

• Monday is a day without classes at EPFL
• Tuesday 16:15 in INM 10: Tree Automata. Semantics of Procedures (half-lecture)
• Tuesday 17:15 in INM 200: James A. Whittaker, Engineering Director: “How Google Tests Software?”
• Friday, 10:15: Lecture 18: Specified Procedures

Week 15¹⁾, May 31

• Monday 14:15: Lecture 19: Automated Analysis of Procedures
• Tuesday 16:15: Swen Jacobs lecture
• Friday 10:15: Lecture 20

Week 16

• Project Presentations on June 10