Spring 2014 CS388s Advance Syllabus
T Th 5-6:30pm Formal Verification and Semantics
E. A. Emerson
www.cs.utexas.edu/~emerson/
emerson@cs.utexas.edu
There is a growing need for effective methods of designing correct computer hardware and software. This is particularly so forsafety critical systems such as automotive embedded systems 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, Formal Methods have been developed based on the use of mathematical logic precision tools for specifying and reasoning about
program correctness. Hardware, software, and design automation companies use formal methods to make their products more reliable and less costly to develop.
This course will survey the basic concepts of formal methods. The emphasis will be on the mathematical theory of program veriﬁcation. Some attention will be paid
to applications of the theory.
TOPICS:
1) Preliminaries: Discrete math,logic, fixpoints, automata, Kripke structures
2) Verification of Sequential and Nondeterministic Programs:
-Flowchart programs: invariants,well-founded sets.
-Assertional reasoning: partial and total correctness, compositionality.
-Predicate transformers: weakest precondition calculus: wp, wlp.
3) Verification of Concurrent and Reactive Programs:
-Linear temporal logic: LTL – G (always), F (sometime), X (nexttime), etc.
-Branching temporal logics: CTL, CTL*, Mu-calculus
-Model checking –- algorithmic verification of nominally finite state systems
---Tarski-Knaster theorem for branching time;
---language containment for linear time.
---state explosion: The problem and some solutions.
4) As time permits advanced topics from:
-expressiveness
-linear time vs. branching time
-tableaux for testing satisfiability
-translating tableau into automata
-BDDs – Binary Decision Diagrams for symbolic model representation
-abstraction techniques: homomorphisms, bisimulations, symmetry, etc.
-program synthesis
TEXTS:
Recommended: Huth and Ryan, Logic for Computer Science.
GRADING POLICY:
Participation: 50%
Research/Expository Project and 15 page written Report: 50%