Synthesis, Analysis, and Verification 2013
For Moodle page: click here
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.
- 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 05 Refinement and Synthesis: From Formulas to Programs
- Tue: Labs 02 (Etienne): Work on Previous Lab
- Fri: Labs 02 (Etienne): Finish the Previous Lab
- Friday, 5 April: Labs 03 Due
- 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
- Friday, 31 May: Project Presentations, 9am
- Monday, 10 June: Project Write-Ups and Code Due, 11:55pm