Taught in Spring 2009 by LARA group.

Course Information (see also last year's course)

Contacts: Viktor Kuncak, Ruzica Piskac, Philippe Suter (emails use standard EPFL email convention)

This moodle page is available for uploading your solutions.

- Week 01, February 16
- Lecture 01: Introduction and Background
- Exercises 01: Propositional and First-Order Logic
- Labs 01: Illustration of a Simple Verification System
- Homework 01: Manipulating Propositional Logic Formulas

- Week 02, Febraury 23
- Lecture 02: From Programs to Relations
- Exercises 02: Proving Programs by Translations to Relations and Checking Relation Subset
- Labs 02: Using Alloy to Find Examples of First-Order Logic and Relational Calculus Formulas
- Homework 02: Program to Compute Relations for Loop-Free Code. Paper: Proving Validity and Finding Counterexamples of Statements on Relations and FOL

- Week 03, March 2
- Lecture 03: Hoare Logic Using Relations
- Lecture 03a: Higher-Order Logic
- Labs 03: Illustration of the LCF Approach to Theorem Proving
- Talk by Stefan Staber in the Tresor Seminar: Functional verification of industrial hardware designs using OneSpin 360 MV
- Exercises 03: Simple Proofs. Brief Discussion of Projects

- Week 04, March 9
- Lecture 04: Generating Formulas from Programs: Formulas for Relations. Symbolic Execution
- Lecture 04a: Loops with Supplied Invariants. Meaning of Assert.
- Exercises 04: Substitution theorem. One-point rule. sp using range and composition.
- Labs 04: Individual project discussions

- Week 05: March 16
- Note the tresor talk: Separation Logic Verification of C Programs with an SMT Solver, by Matko Botincan on Monday, 14:15
- Lecture 05: Reasoning about References and Arrays

- Week 06: March 23
- tresor talk: Model-Based Testing Using Test Abstractions, by Darko Marinov, Tuesday, 11:00
- tresor talk: Software model checking for Confidentiality, by Pavol Cerny, on Tuesday, 16:15
- Lecture 06: Abstract Interpretation
- Lecture 06a: More on Abstract Interpretation

- Week 07: March 30
- Lecture 07: Abstract Interpretation through Interval Analysis
- Project discussions

- Week 08: April 6
- Lecture 08: More Techniques and Examples of Abstract Interpretation. Starting DPLL
- Lecture 08a: DPLL

- Week 09: April 20
- Wednesday, April 22:
**Deadline to submit a paper that you will present** - Lecture 09: Quantifier Elimination (in BC 01)
- Lecture 09a: More Quantifier Elimination (in BC 01)
- Thursday 16:15: Tresor talk by Prof. Maria Paola Bonacina (in BC 01)

- Week 10: April 27
- Lecture 10: WS1S Decision Procedure (in BC 01)
- Exercises 10: on Thursday, April 30, 14:05-18:00
**round 1 of paper presentations**(in BC 355)

- Week 11: May 4
- Lecture 11: Quantifier-Free FOL. Nelson-Oppen and DPLL(T) (in BC 01)
- Exercises 11: on Thursday, May 7, 14:05-18:00
**round 2 of paper presentations**(in BC 01)

- Week 12, May 11
- Lecture 12 Combining Decision Procedures. Basics of Resolution
- Lecture 13 Resolution marathon

- Week 13, May 18
- Lecture 14: Resolution and Equality. EPR (given by Ruzica)
- Thursday: holiday

- Week 14, May 25
- Lecture 15: Interprocedural analysis: contracts, context-free reachability, set constraints
- Exercises 15 on Thursday:
**project presentations**in BC 355

- June 5: Submit
**project reports**(see Academic Calendar)- 4-8 pages of length (in double-column format)
- similar style to the papers you presented
- submit your solution to the Wiki of your project, either
- upload a PDF file (e.g. produced by pdflatex or latex+ps2pdf), or
- enter the report directly in wiki (feel free to use links, but try to make it as self-contained as possible, so it is meaningful even if the links break)

- feel free to send us a draft of the project report before the deadline: we will give you feedback so you can improve the final version