====== Synthesis, Analysis, and Verification 2010 ======

Next edition: [[sav11:top|Synthesis, Analysis, and Verification 2011]]

[[Course Information]]
  * [[http://infowww.epfl.ch/imoniteur_ISAP/!itffichecours.htm?ww_i_matiere=51680512&ww_x_anneeAcad=2009-2010&ww_i_section=249847&ww_i_niveau=&ww_c_langue=en|Course in the Catalog]]
  * [[sav09:top|2009 Edition]]
  * [[sav08:intro|2008 Edition]]

[[http://moodle.epfl.ch/course/view.php?id=5171|Moodle Page for Homework Submission]]


===== Course Material =====

Week 01, February 22
  * [[Lecture 01]]
  * [[Exercises 01]] in [[http://plan.epfl.ch/?lang=en&room=INM10|INM10]]
  * [[Homework 01]]
  * Some relevant easy reading, from CACM:
    * [[http://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext|A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World]]
    * [[http://cacm.acm.org/magazines/2009/10/42360-retrospective-an-axiomatic-basis-for-computer-programming/fulltext|Retrospective: An Axiomatic Basis for Computer Programming]]
    * [[http://cacm.acm.org/magazines/2009/11/48424-model-checking-algorithmic-verification-and-debugging/fulltext|Model Checking: Algorithmic Verification and Debugging]]
    * [[http://cacm.acm.org/magazines/2010/2/69362-software-model-checking-takes-off/fulltext|Software Model Checking Takes Off]]
    * [[http://cacm.acm.org/magazines/2009/7/32099-formal-verification-of-a-realistic-compiler/fulltext|Formal Verification of a Realistic Compiler]]
    * [[http://cacm.acm.org/magazines/2010/6/92498-sel4-formal-verification-of-an-operating-system-kernel/fulltext|seL4: Formal Verification of an Operating-System Kernel]]
      * [[http://cacm.acm.org/magazines/2010/6/92462-learning-to-do-program-verification/fulltext|Learning To Do Program Verification]] - a foreword by K. Rustan M. Leino
Week 02, March 01
  * [[Exercises 02]]
  * [[Lecture 02]]
  * Talk [[http://tresor.epfl.ch/dokuwiki/seminars|Model Checking High level Petri Nets]] in [[http://plan.epfl.ch/?room=BC355|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: [[https://tresor.epfl.ch/dokuwiki/seminars|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 [[https://tresor.epfl.ch/dokuwiki/seminars|talk by Prof. Peter Mueller (EHTZ)]]
  * [[Exercises 06]]
  * [[Homework 03]]
  * [[invariants exercises|Invariants Space]]

Week 07, April 5 - Spring Break

Week 08, April 12
  * Monday: [[Lecture 07]]: Abstract Interpretation
  * Tuesday: [[https://tresor.epfl.ch/dokuwiki/seminars|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: {{sav10:synthesislia.pdf|Lecture 11, slides}}
  * Tuesday, 16:15 [[https://tresor.epfl.ch/dokuwiki/seminars|talk by David Monniaux (VERIMAG, Grenoble)]],\\
 -> see the paper [[http://doi.acm.org/10.1145/1480881.1480899|Automatic modular abstractions for linear constraints]] in [[http://portal.acm.org/toc.cfm?id=1480881&type=proceeding&coll=GUIDE&dl=GUIDE&CFID=85528772&CFTOKEN=86443673|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|Lecture 13: Modeling and Proving Properties about Sets and Data Structures]]
  * Tuesday 16:15 [[Lecture 14|Lecture 14: Reasoning about Reachability and Introduction to WS1S]]

Week 13, May 17
  * Monday 14:15 [[Lecture 15|Lecture 15: Decision Procedure for WS1S]]
  * Tuesday 16:15: Individual work
  * Friday 10:00 [[Lecture 16|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: [[Lecture 17|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|Lecture 18: Specified Procedures]]

Week 15((it's 15 because we counted Spring break)), May 31
  * Monday 14:15: [[Lecture 19|Lecture 19: Automated Analysis of Procedures]]
  * Tuesday 16:15: Swen Jacobs lecture
  * Friday 10:15: [[Lecture 20|Lecture 20]]

Week 16
  * Project Presentations on June 10