Tentative Syllabus


Fall 2008                           cs388s:                Unique no.: 55855
TTh 5-6:30p               Formal Verification and Semantics
WEL3.402 (may change)                 
emerson@cs.utexas.edu              E. A. Emerson                       

There is a growing need for effective methods of designing correct computer 
hardware and software, particularly for safety critical systems such as 
air traffic control software or for systems that are costly to recall such as 
microprocessors (e.g., the $500M loss by Intel on the Pentium division error.)
To cope with these problems, Computer Aided Verification methods have been 
developed based on the use of logic and automata as precision tools for 
specifying and reasoning about program correctness. 
Major companies such as IBM, Intel, Lucent, Microsoft, Synopsys, Cadence,
and FreeScale use Computer Aided Verification and related formal methods.

This course will survey the classic theory of Formal Verification,
including the work of Floyd, Hoare, and Dijkstra.
Related work on Computer Aided Verification, including the work of
Pnueli, Emerson, Clarke, Sifakis, and Milner are also addresses. The emphasis 
will be on using and applying logic, lattice theory, and automata theory 
to program verification and semantics.



TOPICS:

Preliminaries:
  Discrete math, logic, automata, transition systems;
Verification of Sequential and Nondeterministic Programs:
  Floyd's method: invariants, well-founded sets
  Hoare's logic: compositionality, partial and total correctness
  Dijkstra's weakest precondition calculus: wp, wlp
Verification of Concurrent and Reactive Programs:
  Linear temporal logic: G (always), F (sometime), X (nexttime), etc.;
  Branching time temporal logics CTL, CTL*
  Model checking: by Tarski-Knaster theorem for branching time;
                  by finite automata on infinite strings for linear time
  State explosion: the problem and some solutions
  
As time permits advanced topics from:
  Linear time vs. Branching time temporal logics
  Tableau for testing satisfiability and automata construction
  Binary Decision diagrams for symbolic model checking   
  Abstraction techniques: homomorphisms, bisimulations, symmetry, etc.

TEXTS:
  Recommended:
    Huth and Ryan, Logic for Computer Science
    Berard et al, Systems and Software Verification: Model-checking Techniques
                  and Tools

GRADING POLICY (Provisional):
  Homework/Quizzes: 25%
  Class Participation: 25%
Project 50%
  No final exam