Synthesis, Analysis, and Verification 2013

For Moodle page: click here

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:

• Etienne
• Eva
• Viktor

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

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

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

• 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

• Mon: Lecturecise 06 (Viktor): Modeling Loops and Recursion
• Tue: Lecturecise 07 (Filip): Exact Transitive Closure - Acceleration
• Fri: Labs 03 (Etienne)

• Mon: Lecturecise 08 (Viktor): Fixpoints. Algebraic Data Types
• Tue: Lecturecise 09 (Eva): Hoare Logic with exercises
• Fri: Finishing Labs (Etienne)

• 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

• Friday, 5 April: Labs 03 Due

• 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

• 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

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

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

• 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

• 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

• Monday, 20 May: No classes
• Tuesday, 21 May: Lecturecise 22: Monadic Second-Order Logic
• Friday, 24 May: Lecturecise 23: SMT Solvers

• 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

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