Synthesis, Analysis, and Verification (SAV) 2015
Link to Moodle (please sign up)
Instructors:
- Viktor Kuncak, Associate Prof., EPFL
- Ondrej Lhotak, Associate Prof., Waterloo
Teaching assistants:
Software:
For a flavor of this course, see all the materials in SAV 2013
Location of INR113 Location of INM10
EXAM TENTATIVE DATE: Wednesday, 22 April, INR 113 from 13:15
Week 01
| Wednesday 13:15 | INR 113 | Lecture 01: Introduction |
| Wednesday 15:15 | INR 113 | Exercise 01: Logic, sets and relations |
| Friday 15:15 | INM 010 | Labs 01: Using Leon to Make Programs Verify |
Week 02
| Wednesday 13:15 | INR 113 | Lecture 02: Presburger Arithmetic and Quantifier Elimination |
| Wednesday 15:15 | INR 113 | Labs 02: Using Leon to Develop Verified Programs |
| Friday 15:15 | INM 010 | Lecture 03: From Programs to Formulas |
Week 03
| Wednesday 13:15 | INR 113 | Lecture 04: Equivalence, Refinement, and Synthesis from Relations |
| Wednesday 15:15 | INR 113 | Labs 03: More Leon Verification |
| Friday 15:15 | INM 010 | Lecture 05: Hoare Logic, Strongest Postcondition and Weakest Precondition |
Week 04
| Wednesday 13:15 | INR 113 | Lecture 06: Propagating Preconditions and Postconditions |
| Wednesday 15:15 | INR 113 | For Project Suggestions, see Moodle |
| Friday 15:15 | INM 010 | Lecture 07: Loops and Recursion |
Week 05
| Wednesday 13:15 | INR 113 | Lecture 08: More Recursion. Bounded Checking Ideas. SAT |
| Wednesday 15:15 | INR 113 | Lecture 09: Satisfiability Modulo Theories |
| Friday 15:15 | INM 010 | Labs: Discussion of projects |
Week 06
| Wednesday 13:15 | INR 113 | Lecture 10: Constraint-Based Analysis |
| Wednesday 15:15 | INR 113 | Labs: Working on Projects |
| Friday 15:15 | INM 010 | Lecture 11: Abstract Interpretation |
Week 07
| Wednesday 13:15 | INR 113 | Lecture 12: Abstract Interpretation continued |
| Wednesday 15:15 | INR 113 | Paper Discussion Paper A: John B. Kam, Jeffrey D. Ullman. Monotone Data Flow Analysis Frameworks. Acta Inf. 7. 305-317 (1977), pdf |
| Wednesday 16:15 | INR 113 | Labs: Working on Projects |
Friday is a holiday.
Then there is a week without classes.
Week 08 (Starting Monday 13 April 2015)
| Wednesday 13:15 | INR 113 | Paper Discussion: Paper B. Micha Sharir, Amir Pnueli: Two Approaches to Interprocedural Data Flow Analysis, pdf |
| Wednesday 15:15 | INR 113 | Labs: Working on Projects |
| Friday 15:15 | INM 010 | (Short) Lecture 13: Predicates and Intervals |
| INM 010 | Quiz Exercises |
Week 09 (Starting Monday 20 April 2015)
| Wednesday 13:15 | INR 113 | Quiz |
| Wednesday 15:15 | INR 113 | Quiz |
| Friday 15:15 | INM 010 | Labs: Working on Projects |
Week 10 (Starting Monday 27 April 2015)
| Wednesday 13:15 | INR 113 | Paper Discussion: Papers C and D |
| Wednesday 16:00 | INR 113 | Labs: Working on Projects |
| Friday 15:15 | INM 010 | Labs: Working on Projects |
Week 11 (Starting Monday 4 May 2015)
| Wednesday 13:15 | INR 113 | Paper Discussion: Papers E and F |
| Wednesday 16:00 | INR 113 | Labs: Working on Projects |
| Friday 15:15 | INM 010 | Labs: Working on Projects |
Week 12 (Starting Monday 11 May 2015)
| Wednesday 13:15 | INR 113 | Paper Discussion: Papers G and H |
| Wednesday 16:00 | INR 113 | Labs: Working on Projects |
| Friday 15:15 | INM 010 | No Labs |
Week 13 (Starting Monday 18 May 2015)
| Wednesday 13:15 | INR 113 | Paper Discussion: Papers I and J |
| Wednesday 16:00 | INR 113 | Labs: Working on Projects |
| Friday 15:15 | INM 010 | Labs: Working on Projects or Project Presentations ? |
Week 14 (Starting Monday 25 May 2015)
| Wednesday 13:15 | INR 113 | Project Presentations |
| Wednesday 15:15 | INR 113 | Project Presentations |
| Friday 15:15 | INM 010 | Project Presentations |
Type systems:
—-