Spring 2008
CS 477: Formal Software Development Methods
09:30am-10:45am, Tuesdays and Thursdays
1103 Siebel Center

Verified hardware and software is one of the grand challenges of computer science. As the complexity of systems increases and as computers pervade our day-to-day activities, verification of systems ranging from cell phones to medical equipment to aircraft software to secure programs, has become a vibrant and important field.

This course is a general introduction to the field of formal verification. If you are interested in verification in general, this course is for you. If you are working in a field such as security or software engineering or AI or databases, this course will provide an overview of tools and techniques that you may find use in your own field. In particular, you will learn of some of the exciting tools to search large state spaces (using BDDs), tools to solve complex theorems automatically (automatic theorem provers), and tools to solve "real-life" large NP-complete problems (SAT solvers).

The field of verification is almost as old as computer science; some concepts such as the Floyd-Hoare style of verification is 40 years old. And yet the field has become a vibrant area of research only in the last 20 years, and has matured in this period so much that hardware verification is routinely done in the industry, and software verification tools such as Microsoft's SDV (and SLAM) are at the level where they can be deployed automatically to check software. All this has been based on a few fundamental techniques and tools, which we will learn in this course.

We will start with basic finite models of systems, and show how to verify them, and slowly move to more and more complex models such as finite systems with recursion, and finally full-fledged software verification.

The topics we will cover are:

  • 1. Finite models and model-checking - Modeling using finite models, reachability algorithms
  • 2. Specification logics - LTL on finite words; automata theoretic model checking algorithms, the SMV tool
  • 3. Dataflow analysis of programs without recursion
  • 4. Handling recursion: pushdown models, reachability (using games!), dataflow analysis.
  • 5. Symbolic methods for reachability: Boolean Decision Diagrams, operations on BDDs, the tools SMV and Mucke
  • 6. CTL and CTL model-checking symbolically; mu-calculus (alternation depth 1!)
  • 7. Software verification: The Floyd-Hoare method for verifying code
  • 8. Invariant verification using automatic theorem provers: The Boogie tool
  • 9. Testing programs: Random testing and directed testing using symbolic evaluations
  • 10. Satisfiability solvers (SAT solvers); bounded model checking and testing.
  • 11. Abstraction based model checking
  • 12. Miscellaneous topics:
  • - Decidable logics and overview of available theorem provers
  • - Predicate abstraction and abstract interpretation
  • - Handling heaps
  • - Concurrency!
    • You will learn to use some tools:
  • - A BDD-based model-checker for finite and pushdown systems (SMV and/or Mucke)
  • - A software invariant verification tool (Boogie, from Microsoft Research)
  • - A SAT solver
    • As for theory, you will learn temporal and first order logics, automata based verification, Floyd-style verification, decision procedures and satisfiability solving.

    See the course here for a course that covered some of these topics (though in more detail) in Spring 2005. This course will be a more gentle introduction and will cover a wider variety of verification methods, and will have a significant tool component.

    References:
  • Model Checking: Clarke, Grumberg, Peled. MIT Press.
  • Ken McMillan's thesis
  • Reasoning About Infinite Computations (Godel Award, 2000!)
  • Linear-Time Temporal Logic and Buchi Automata, tutorial notes by Madhavan Mukund. (Also available locally here.)
  • Bounded Model Checking, by Biere, Cimatti, Clarke, Strichman, Zhu.
  • The Quest for Efficient Boolean Satisfiability Solvers , Zhang and Malik. (Springer link; downloadable from UIUC IP addresses).
  • Applying SAT Methods in Unbounded Symbolic Model Checking , by McMillan -- Sections 2 and 3 are useful to understand how SAT works.
    • News:
  • Turing Award 2007 goes to Ed Clarke, Allen Emerson and Joseph Sifakis for their work in model-checking! See ACM announcement
  • Homework#1 released (Jan 31); due Feb 14.
  • Homework#2 released (Mar 13); due Apr 1.
  • Final exam will be a take-home exam from May 2nd to May 7th; due on May 7th by 3pm.
    • Homeworks:
    Homework Number Date posted Date due Homework handout
    1 1/31 2/14 Homework #1 (pdf)
    2 3/13 4/1 Homework #2 (pdf)

    Lectures
    Lec Num Date Material covered Lecture notes Readings/Handouts/Hyperlinks Comments
    1 1/15 Administrivia, overview, motivation Lecture 1 (pdf)    
    2 1/17 Modeling Systems Lecture 2 (pdf) Handout given out in class  
    3 1/22 Reachability, BDDs Lecture lost (system crash!) Handout given out in class Installing NuSMV
    4 1/24 Operations on BDDs Lecture 4 (pdf)    
    5 1/29 CTL; Model-checking CTL on an explicit graph All lecture on white board    
    6 1/31 CTL model checking using BDDs; NuSMV; Reachability games on finite graphs; BDD based game solving Lecture 6 (pdf)    
    7 2/5 Automata on infinite words; introduction to LTL Lecture 7 (pdf)    
    8 2/7 LTL -> Automata; LTL model checking Lecture 8 (pdf) Handout from Madhavan Mukund's Tutorial (see References)  
    9 2/12 SAT and bounded model checking
    Reachability, lasso reachability, LTL    		 Lecture 9 (pdf) BMC paper  
    10 2/14 Internals of a SAT solver      
    11 2/19 Dataflow analysis/Static analysis
    Introduction, Reaching-definition     		Lecture 11 (pdf)    
    12 2/21 Dataflow analysis/Static analysis - II
    Formalizing dataflow analysis; kill/gen functions
    Very-busy expr; may/must analysis    		 Lecture 12 (pdf)    
    13 2/26 Dataflow analysis/Static analysis - III
    Lattices, fixpoints, distributive flows, constant-propagation, meet-over-paths, MFP=MOP for distributive flows    		      
    14 2/28 Meet-over-paths analysis using automata
    Inter-procedureal flow analysis using pushdown automata    		 Lecture 14 (pdf)    
    15 3/4 Reachability Analysis of Pushdown Automata using Games Lecture 15 (pdf)    
    16 3/6 Interprocedural analysis exploiting distributive problems Lecture 16 (pdf)    
    17 3/11 Flow-insensitive pointer-analysis by Steensgaard      
    18 3/13 Review of topics covered, and lookahead of topics to be covered; Discussion of projects      
    19 3/25 Floyd's framework for program verification; Invariants      
    20 3/27 Floyd's framework (contd.) and Hoare's axioms      
    21 4/1 Introduction to abstract reasoning of programs through examples      
    22 4/3 Predicate abstraction and introduction to abstract interpretation      
    23 4/8 Abstract Interpretation Formalism for abstract reasoning Lecture 23 (pdf)    
    24 4/10 Predicate Abstraction II: Generating abstract programs using theorem provers      
    25 4/15 Generating test inputs; Symbolic evaluation      
    26 4/17 Overview of course; exam details Review slides    
    27 4/22 Decision procedures; Quantifier elimination; Fall course on logic in computer science
    Project presentation by Long Wang    		      
    28 4/24 Project presentations by Brandon Moore and Abdullah Al-Nayeem      
    29 4/29 Project presentation by Vijay Anand Korthikanthi