Synthesis, Analysis, and Verification 2013

The course will be similar to SAV 2012 and 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 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:

Schedule

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

-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 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 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
• 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

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 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