Madhavan Mukund

Verification

Aug-Nov, 2011

Text Book

• Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press (2008).

Resource material

Spin and Promela

• Using Spin
  G Holzmann
  Plan 9 Programmer's Manual Documents, pp. 353-382, Vita Nuova Holdings Ltd, York England. 1st edition 1995, 2nd edition, 2000.

• Design and Validation of Computer Protocols
  Gerard J Holzmann
  Prentice-Hall, 1991
  

Büchi automata and LTL

• Finite-state Automata on Infinite Inputs
  M Mukund
  Modern Applications of Automata Theory
  Deepak D'Souza and Priti Shankar (eds), World Scientific (2011) to appear.

• Linear-Time Temporal Logic and Büchi Automata
  M Mukund
  Tutorial talk, Winter School on Logic and Computer Science, ISI, Calcutta, January 1997.

Binary Decision Diagrams

• An Introduction to Binary Decision Diagrams
  Henrik Reif Andersen
  

Timed Systems

• A Theory of Timed Automata
  Rajeev Alur and David Dill
  Theoretical Computer Science 126(2) (1994) 183-235.

• Decision problems for timed automata: A survey
  Rajeev Alur and P Madhusudan
  4th Intl. School on Formal Methods for Computer, Communication, and Software Systems: Real Time (2004).

Uppaal

• Uppaal 4.0 : Small Tutorial

• A Tutorial on Uppaal
  Gerd Behrmann, Alexandre David, and Kim G Larsen.

Lectures

• Lecture 1, 11 August 2011

  Chapter 2.1: Transition systems

  • Basic definitions
  • Examples: Beverage vending machine, sequential hardware circuits, data dependent systems
  • Program graphs and their associated transition systems

• Lecture 2, 16 August 2011

  Chapter 2.2: Parallelism and Communication

  • Interleaving of transition systems
  • Shared variables and interleaving of program graphs
  • Handshaking on shared actions
  • Message-passing (introduction)

• Lecture 3, 19 August 2011

  Chapter 2.2.4: Parallelism and Communication

  • Message-passing
  • Alternating Bit Protocol

• Lecture 4-5, 26 August 2011

  Chapter 3: Linear Time Properties

  • Paths and Traces
  • Invariants, Safety, Liveness
  • Safety vs Liveness
  • Fairness

• Lecture 6-7, 2 September 2011

  Chapter 5: Linear Temporal Logic

  • Syntax (5.1.1)
  • Semantics (5.1.2)

  Chapter 4: Regular Properties Logic

  • Model-checking Regular Safety Properties (4.2)
  • Automata on infinite words (4.3)

• Lecture 8-9, 9 September 2011

  Chapter 4: Regular Properties Logic

  • Model-checking ω-regular Safety Properties (4.4)

  Chapter 5: Linear Temporal Logic

  • Equivalence of LTL formulas, Weak Until, Release, Positive Normal form (5.1.4-5.1.5)
  • Automata-based LTL model checking

• Lecture 10, 13 September 2011

  An introduction to Promela and Spin

  • Basic datatypes, bit/bool/short/int/unsigned
  • Guarded commands, do..od, if..fi, else, break
  • Statement labels, goto
  • Process creation, implicit (active proctype) and explicit (run)
  • Assertions
  • LTL properties
  • Invoking Spin: random simulation, creating a verifier (pan.c), guided simulation (trail)

• Lecture 11, 22 September 2011

  More about Spin

  • Channels
  • Deadlock vs termination

• Lecture 12-13, 23 September 2011

  Chapter 6: Computation Tree Logic

  • Syntax and semantics of CTL, derived operators, normal forms (6.2)
  • (In)expressivity results, CTL vs LTL (6.3)
  • CTL model-checking algorithm, overview

• Lecture 14-15, 7 October 2011

  Chapter 6: Computation Tree Logic

  • CTL model-checking --- lfp and gfp interpretation (6.4)
  • Quick introduction to symbolic model checking

• Lecture 16, 18 October 2011

  Chapter 6: Computation Tree Logic

  • Symbolic model checking and BDDs (6.7)
  • Using boolean functions for model-checking (6.7.1-6.7.2)
  • Definition of OBDDs and ROBDDs (6.7.3)

• Lecture 17-18, 21 October 2011

  Chapter 6: Computation Tree Logic

  • Symbolic model checking and BDDs (6.7)

    • ROBDDs: canonicity and completeness (6.7.3)
    • Structural rules for reducing OBDDs (6.7.3)
    • Inductive construction of ROBDDs using ITE operator (6.7.4)
    • Computing relational product (used in fixed-point computation for model-checking) (6.7.4)

  • CTL^* (6.8)

    • Syntax and semantics
    • Model checking

  Chapter 5: Linear Temporal Logic

  • Some lower bounds for LTL (5.2)

• Lecture 19-20, 01 November 2011

  Chapter 9: Timed Automata

  • Timed automaton (9.1)
  • TCTL, syntax and semantics (9.2)
  • The region construction (9.3.3)
  • Non-closure under complementation (Alur-Madhusudan survey)

• Lecture 21, 03 November 2011

  Chapter 9: Timed Automata

  • TCTL model-checking (9.3)

  Introduction to Uppaal

• Lecture 22-23, 15 November 2011

  Chapter 7: Equivalences and abstraction

  • Bisimulation
  • Basic definitions (7.1)
  • CTL* characterization (7.2)
  • Basic partition refinement algorithm (7.3.1-7.3.3)
  • Simulation
  • Basic definitions (7.4)
  • ∀CTL* characterization (7.5)
  • Basic partition refinement algorithm (7.6, initial part)
  • Stutter equivalence
  • Stutter traces and LTL\O (7.7)
  • Stutter bisimulation, divergence, CTL\O (7.8.1,7.8.3)