Organisation

• Laure Gonnord (LYON1, LIP) and David Monniaux (CNRS, VERIMAG). On Tuesday afternoons 13h15-16h15

Slides

• Course #1: intro/sat/bdd and program analysis with sat/smt
• Course #2: bdd exercises. DataFlow, Abstract Interpretation (numerical domains). abs. int. exercises.
• LAB 1 + project : ia.pdf. APRON ocaml interface. The project is due on October, 24, 23:59 (email)
• LAB 2 : demo + pdf. Companion files.
• Papers : archive with howto+examples. List of all papers with assignment.
• Course #3: data structures.
• Course #4: Astree and WCET.
• Paper session on 6/12 and 7/12 : allocation and schedule

Outline

• Plan + biblio
• Introduction, bounded model-checking, SAT, SMT.
• Abstract interpretation and various abstract domains.
• Application to software verification, termination, compilation.
• Scalability issues.
• Two labs and a program analysis project.

Schedule 2016-17