====== Synthesis, Analysis, and Verification 2013 ======

For Moodle page: [[http://moodle.epfl.ch/course/view.php?id=13051|click here]]

The course will be similar to [[sav12:top|SAV 2012]] and [[sav11:top|SAV 2011]].
(See there for overview as well.)

We initially refresh our knowledge of logic and agree on notation, but for a more thorough introduction, in addition to many textbooks, you may wish to check the videos of [[https://class.coursera.org/intrologic//lecture/preview|Introduction to Logic]] course at Coursera.

Grading scheme is weighted average rounded to half-grades using a linear non-homogeneous function:
  * 30% common project in first part of semester (in stages and feedback after each, but grade only after all of them)
  * 40% quiz in 2nd part of semester
  * 30% individual projects by the project deadline

Main changes compared to SAV 2012 is a little more focus on verifying recursive functional programs over imperative programs. This will also include some reordering of the material, including descriptions of fixpoints and recursion earlier, as well as earlier coverage of quantifier elimination.

Teaching staff:
  * [[http://people.epfl.ch/etienne.kneuss|Etienne]]
  * [[http://people.epfl.ch/eva.darulova|Eva]]
  * [[http://lara.epfl.ch/~kuncak/|Viktor]]

==== Schedule ====

  * Monday 14:15-16:00
  * Tuesday 16:15-18:00
  * Friday 10:15-12:00

{{sav13:sav13-schedule.png?960|Synthesis, Analysis, and Verification 2013 Schedule}}

----

-And how many hours a day did you do your lessons?

-Ten hours the first day, nine the next, and so on.

-What a curious plan!

-That's the reason they're called lessons, because they lessen from day to day.

----

==== Week 01 ====

  * Mon: [[Lecturecise 01]] (Viktor): **Introduction**
  * Tue: [[Lecturecise 02]] (Eva): Logic, sets and relations
  * Fri: [[Labs 01]] (Etienne): Breaking Leon online

==== Week 02 ====
  * Mon: [[Lecturecise 03]] (Viktor) - **Presburger Arithmetic and Quantifier Elimination**
  * Tue: [[Labs 02]] (Etienne): Break your own Leon (in INM10, bring your own laptops!)
  * Fri: [[Lecturecise 04]] (Viktor) **From Programs to Formulas (VCG)**

==== Week 03 ====
  * Mon: [[Lecturecise 05]] **Refinement and Synthesis: From Formulas to Programs**
  * Tue: Labs 02 (Etienne): Work on Previous Lab
  * Fri: Labs 02 (Etienne): Finish the Previous Lab

==== Week 04 ====
  * Mon: [[Lecturecise 06]] (Viktor): **Modeling Loops and Recursion**
  * Tue: [[Lecturecise 07]] (Filip): **Exact Transitive Closure - Acceleration**
  * Fri: [[Labs 03]] (Etienne)

==== Week 05 ====
  * Mon: [[Lecturecise 08]] (Viktor): **Fixpoints. Algebraic Data Types**
  * Tue: [[Lecturecise 09]] (Eva): **Hoare Logic** with exercises
  * Fri: Finishing Labs (Etienne)

==== Week 06 ====

  * Mon: [[Lecturecise 10]]: **Weakest Preconditions. Algebraic Data Types**
  * Tue: [[Lecturecise 11]] (Tihomir Gvero and Ivan Kuraj): **Type-Driven Synthesis**
    * **[[Project suggestions]]**
  * Friday 29 March: NO CLASS

=== Spring Break ===

  * Friday, 5 April: Labs 03 Due

==== Week 07 ====

  * Monday, 8 April: [[Lecturecise 12]]: **Abstract Interpretation Ideas**
  * Tuesday, 9 April: [[Lecturecise 13]]: **Lattices**
  * Wednesday, 10 April: Project Descriptions Due
  * Friday, 12 April: Labs: ask questions about your project


==== Week 08 ====
  * Monday, 15 April: [[Lecturecise 14]]: **From Lattices to Abstract Interpretation**
  * Tuesday, 16 April: [[Lecturecise 15]] (Philippe): **SAT solving**
  * Friday, 19 April: [[Lecturecise 16]]: **Computing Interval Bounds, Chaotic Iteration, Widening and Narrowing**


==== Week 09 ====

  * Monday, 22 April: Labs
  * Tuesday, 23 April: [[Lecturecise 17]]: **Predicate Abstraction**
  * Friday, 26 April: [[Lecturecise 18]]: **Bounded Model Checking, k-induction. Interpolation**

==== Week 10 ====

  * Monday, 29 April, [[Practice quiz]]
  * Tuesday, 30 April: Labs
  * Friday, 3 May: **QUIZ**, 8am - 12pm in **INR 113**

==== Week 11 ====
  * Monday, 6 May: Quiz Solutions and Discussion
  * Tuesday, 7 May: Labs and Discussion of Results
  * Friday, 10 May: [[Lecturecise 19]]: **Compactness and Normal Form Theorems**

==== Week 12 ====
  * Monday, 13 May: [[Lecturecise 20]]: **Herbrand's Theorem and Resolution for FOL**
  * Tuesday, 14 May: [[Lecturecise 21]]: Finished Resolution Example. Decidable EPR Fragment. Encoding Set Algebra. Deciding Quantifier-free BAPA
  * Friday, 17 May: No official labs: schedule meetings with us about the project

==== Week 13 ====
  * Monday, 20 May: **No classes**
  * Tuesday, 21 May: [[Lecturecise 22]]: **Monadic Second-Order Logic**
  * Friday, 24 May: [[Lecturecise 23]]: **SMT Solvers**

==== Week 14 ====
  * Monday, 27 May: [[Lecturecise 24]]: **Modeling Arrays and Linked Structures**
  * Tuesday, 28 May: No official labs: schedule meetings with us about the project
  * Friday, 31 May: [[PROJECT PRESENTATIONS]] 9:00am - 12:00pm in **INR 113**

==== Important dates ====

  * Friday, 31 May: **Project Presentations**, 9am
  * Monday, 10 June: **Project Write-Ups and Code Due**, 11:55pm