Organisation

  • Laure Gonnord (LYON1, LIP) and David Monniaux (CNRS, VERIMAG)

Slides

Outline

  • Data flow analysis - Constraint based analysis : simple analysis, s.t. pointer analysis
  • Bounded Model-checking, SAT, SMT :
    • effective use of Floyd-Hoare annotations : Lab: Frama-C;
    • decision procedures for Boolean SAT; linear real arithmetic;
    • uninterpreted functions and arrays;
    • Lab : DIMACS SAT format, SMT-LIB.
  • Abstract interpretation basics:
    • Interval and other non relational analyses as extension of data flow analysis
    • Relational domains, e.g. polyhedra
    • Pointers and structures
    • Lab: PAGAI and ConcurInterproc
  • Abstract interpretation, applications
    • Industrial examples: Absint aiT and AstrĂ©e
    • Floating-point and bitvectors
    • Microarchitectural analysis of caches and pipelines, application to WCET
  • Termination:
    • linear and polynomial ranking functions
    • other approaches
  • Scalability of static analyses : SSI