Instructors : Ashutosh Gupta and Paritosh Pandya
Timings : Monday and Wednesday 14:00-16:00
Venue : D405
This is an introductory course for theoretical and practical aspects of verification. In the course, we will cover automata on infinite words, logics for infinite behaviours, timed systems, decision procedures, SMT solving, SAT solvers, abstract interpretation, symbolic model checking, bounded model checking, abstract refinement based model checking. The course work includes theoretical as well as practical exercises.
The course consists of two modules automata theory and software model checking. The theory module will be conducted by Paritosh Pandya (green lectures) and the practice module will be conducted by Ashutosh Gupta (blue lectures).
Introduction and Background Introduction to Formal verification, Program logics and Algorithmic verification. Reactive system modelling.
Logics and Automata over Finite words First order and Monadic second order logic over words. Equivalence of MSO-definable and regular languages. First order definable languages and dot-depth hierarchy. Ehrenfeucht-Fraisse games.
Automata on Infinite Words Omega words. Buchi, Muller, Rabin, Streett automata and reductions between them. Closure properties. Emptiness checking. Determinization.
Temporal Logics Linear versus branching time logics. Computation Trees. Logics CTL*, CTL and LTL. Interval Temporal Logics. Model checking CTL, LTL and CTL*. Fairness.
Symbolic Model Checking Ordered Binary Decision Diagrams and their manipulation. Representing Finite state transition systems using OBDDs and symbolic computation of reachability. Symbolic cycle detection algorithms. Symbolic model checking algorithm for CTL and Mu-Calculus. The SMV verifier. Overview of SAT and SMT-solving. Bounded Model checking.
Theory and verification of Timed Systems Non-deterministic and Deterministic Timed Automata, Region Construction and Emptiness checking, Zone based reachability search and Tool Uppaal. Undecidability of Universality checking, Event Recording Timed Automata and their determinization, Real-time logics: MTL and TPTL.