Lab for Automated Reasoning and Analysis LARA

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.

SAV09 Projects

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
  • Week 06: March 23
  • Week 07: March 30
  • Week 08: April 6
  • Week 09: April 20
  • 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
  • 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
 
sav09/top.txt · Last modified: 2009/05/29 13:30 by vkuncak