Software Analysis and Verification 2009
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.
Course Material and Schedule
- 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