# Synthesis, Analysis, and Verification (SAV) 2015

Instructors:

Teaching assistants:

Software:

For a flavor of this course, see all the materials in SAV 2013

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:

—-