| Date | Topics details |
|---|
| Jul 26 | Introduction, logistics. Examples of
"almost similar" programs that compute very
different results.
An illustration of Floyd-Naur style of proof using
a simple "while" program. |
| Jul 29 | Prerequisites Quiz |
| Aug 2 | Overview of partial orders, lattices and fixed points.
Overview of Tarski's fixed point theorem. |
| Aug 5 | More on fixed points: reflexive transitive closure of
relations as least fixed point. Operational semantics
of programs: configurations, operational transition
relation. |
| Aug 9 | More on operational transition relation:
recursive definition, an example using "while"
programs. | |
| Aug 12 | Relational semantics of programs: definition,
discussion, an example.
Clarifications
| |
| Aug 16 | Relational semantics continued. Assertions,
specifications, partial correctness: Floyd
Naur approach. Stepwise induction method
for Floyd Naur style proofs: role of local
and global invariants and their equivalence with
an example | |
| Aug 19 | Floyd Naur style partial correctness proofs with
stepwise induction:
generating local invariants by pushing precondition
"down" through a program and by hoisting
postcondition "up" through a program |
| Aug 23 | More on stepwise induction method: soundness and
completeness, rules for generating local invariants
from preconditons and postconditions in simple
"while" programs |
| Aug 26 | Introduction to compositional method for
Floyd-Naur style proofs. Quiz 1 |
| Aug 30 | Quiz 1 solution discussion. More on compositional
method for Floyd-Naur style proofs. Introduction
to Hoare Logic |
| Sep 2 | Hoare Logic: Syntax of formulae, examples of
axioms, inference rules, and the idea of
deductive proofs. |
| Sep 6 | Hoare deductive system: Axiom schemata, Inference Rule
schemata, deductive proofs, automatic proof checking
in Hoare deductive system. Hoare proof outlines.
|
| Sep 9 | Hoare proof outlines: examples and practical utility.
Using Hoare Logic in proving partial correctness of
programs with theorem provers.
Importance of loop invariants in program proofs.
A sneak peek into semi-automatic generation of loop
invariants.
|
| Sep 13,
Sep 16 | Mid-semester week |
| Sep 20 | Comments and discussion about Hoare deductive system.
Introduction to model checking: motivation for looking
at finite state systems, definition of Kripke structure.
|
| Sep 23 | Pre-quiz brush-up on Hoare Logic proofs.
Quiz 2. |
| Sep 27 | Discussion of (partial) solution to quiz 2. General
recap of Hoare Logic proof ideas |
| Sep 30 | Modeling a simple concurrent program involving semaphores
using a Kripke structure. Specifying properties of paths
in Kripke structures, Linear Temporal Logic (LTL): syntax
and semantics |
| Oct 4 | Examples and explanations of several LTL formulae expressing
commonly encountered properties of systems. Computation
Tree Logic (CTL): syntax and semantics |
| Oct 7 | Examples of several CTL formulae expressing
commonly encountered properties of systems. Comparison
with LTL, limitations and power of each logic. |
| Oct 11 | CTL model checking with explicit representation of a Kripke
structure, complexity analysis. Illustrative example of
CTL model checking. |
| Oct 14 | Boolean encoding of states in a Kripke structure, representing
sets of states and transition relations using characteristic
functions, computing image and pre-image of state sets using
quantification and conjunction (relational product).
Symbolic breadth-first search (BFS) of a Kripke structure
using characteristic functions, symbolic reachability analysis.
|
| Oct 18 | Binary Decision Diagrams (BDDs) and ROBDDs, manipulating
Boolean functions by graph manipulations in ROBDDs,
basic ROBDD algorithms and their complexities. Use of
ROBDDs in symbolic BFS. |
| Oct 21 | Fixpoint characterizations of CTL operators, CTL model
checking using symbolic fixpoint computation. Illustrative
example for symbolic CTL model checking |
| Oct 25 | LTL model checking by tableau construction: motivation,
intuition and construction of tableau. |
| Oct 28 | More on LTL model checking by tableau construction,
self fulfilling strongly connected components and their
relevance in LTL model checking, using the cross product
of a Kripke structure with the tableau for finding
witness paths. Complexity of LTL model checking,
reducing Hamiltonian path problem to LTL model checking
-- evidence of NP hardness. |
| Nov 1 | Comparison and contrast between LTL and CTL model checking
techniques. Introduction to fairness constraints, fair CTL
model checking, fixpoint characterization of fair CTL
operators, reducing LTL model checking to fair CTL model
checking. |
| Nov 4 | Importance of automatic detection of loop invariants in
proving correctness of programs. Overview of the general
problem of loop invariant computation. Induction-iteration
method a la Suzuki and Ishihata for computing invariants,
weaknesses of the approach. |
| Nov 5 | Detection of linear loop invariants, Cousot and Halbwach's
approach of using widening operator and convex polyhedra for
computing linear loop invariants, illustration with an
example. Summarization of course, and general discussion.
|