Fall 2010
CS 598: Software Verification
3:30pm-4:45pm, Tuesdays and Thursdays
1131 Siebel Center

Scientific methods for engineering reliable software is a grand challenge in computer science. This course is dedicated to studying state-of-the-art techniques for ensuring high reliability of software. We will study several techniques, ranging from testing, type-checking, static analysis, and formal verification, for ensuing correctness to ensure safety and security.

The course will be driven by extensive student presentations of research papers and projects aimed to learn, explore, and perhaps even accomplish new research. The course will involve a project, aligned with the student's research area if possible. Graduate students already working on verification, security, or programming languages, with some basic knowledge of formal methods in verification, are encouraged to attend.

The course will differ from CS476 as we will not be using rewriting techniques, and from CS477 as it will be more in-depth and research-oriented.


References:

  • Floyd's paper
  • Hoare's paper
  • King'76: Symbolic execution
  • DART: Directed Automated Random Testing
  • Abstract Interpretation: Cousot and Cousot 1977
  • Schwarzbach's lecture notes on static analysis
  • Lecture slides by Cousot on abstract interpretation
  • Graf-Saidi: Construction of abstract state graphs with PVS
  • The SLAM story: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft
  • The Das-Dill refinement technique: Successive Approximation of Abstract Transition Relations
  • Getafix: Model-checking pushdown models using fixed-points: Analyzing Recursive Programs using a Fixed-point Calculus
  • Tools:
  • Floyd-Hoare style verification and contract languages
  • Boogie
  • Visual Studio 2010 includes CodeContracts which allows writing contracts for .NET code.
  • VCC - a verifier for concurrent C that uses Boogie.
  • Constraint-solver based symbolic testing
  • PEX from Microsoft generates tests automatically; can exploit .NET code contracts to generate tests satisfying pre-conditions for unit testing.
  • PEX for fun - An online tool that illustrates PEX for educational purposes.
  • A sample program where PEX does not find the error (uncommenting i=1000 shows error)
  • Abstract Interpretation
  • TVLA - supports standard abstract domains as well as shape analysis.
  • ASTREE analyzer used in verification of Airbus flight control software. Commercial product from AbsInt.
  • APRON - library for numerical abstract domains.
  • Interproc analyzer for a toy language using Apron, available with an online interface.
  • Predicate Abstraction
  • SLAM/SDV: A tool for verifying device drivers against Windows APIs
  • Model checking
  • Getafix: model-checking using fixed points
  • Moped
  • Bebop: Part of SLAM/SDV suite

  • News:
  • Sign up for newsgroup at news.cs.illinois.edu; homeworks and announcements will be posted here. Use this also to talk to each other (e.g. for forming groups around projcts).
  • Sign up for the FM mailing list at: http://lists.cs.uiuc.edu/mailman/listinfo
  • Homeworks:
    Homework Number Date posted Date due Homework handout Homework LaTex Source
    1 09/28 10/07 Homework #1 LaTeX source


    Lectures
    Lec Num Date Material covered Slide capture
    1 Aug 24 Introduction Slides#1
    2 Aug 26 Floyd-Hoare verification technique:
    Inductive invariants, strongest post, weakest pre
    Slides#2
    3 Aug 31 Floyd-Hoare verification:
    Hoare rules
    Termination
    Slides#3
    4 Sep 2 Demo of Boogie, by Rajesh Karmani.
    Brief introduction to logic
    FOL, quantifier-free, Godel's theorems, theories.
    Slides#4
    5 Sep 7 Symbolic testing:
    Path constraints, PEX tool and demo
    Slides#5
    6,7 Sep 9, Sep 14 Abstract Interpretation
    General definition; Galois connections;
    static analysis examples (reaching def, constant prop.)
    numerical domains: intervals, octagons, polyhedra
     
    8 Sep 16 Widenings and Narrowings Slides#8
    9, 10 Sep 21, Sep 23 Predicate Abstraction
    Graf-Saidi approach, Cartesian abstraction
    Counter-example guided abstraction refinement; Das-Dill technique
    SLAM examples; ddverify examples and demo
    Slides#9
    12 Sep 28 Model Checking
    Pushdown system model-checking
    Slides#12
    13 Sep 30 Boolean decision diagrams and symbolic model-checking Slides#13