Verification: Theory and Practice 2015

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).

Topics covered in automata theory

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.

Topics covered in Software verification

Topics will be listed within each lecture.

Lectures

01-28 : Lecture 1 - Introduction to verification

02-04 : Lecture 2

02-09 : Lecture 3 - Logic for Software verification

02-11 : Lecture 4 - Program modeling

02-16 : Lecture 5 - Symbolic methods

02-18 : Lecture 6

02-23 : Lecture 7 - SAT solvers

02-25 : Lecture 8

03-02 : Lecture 9

03-04 : Lecture 10

03-09 : Lecture 11 - Decision procedures II

03-11 : Lecture 12 - Lattice theory and fixed points

03-16 : Lecture 13 - Abstract interpretation

03-18 : Lecture 14

03-30 : Lecture 15 - Abstract interpretation (cont.)

Previous two lectures were spilled over.
See (no slides available; look at latest version of the course) of lecture 13.

04-01 : Lecture 16 - Model checking

04-06 : Lecture 17 - Recent topics in software verification

04-08 : Lecture 18

03-13 : Lecture 19

03-15 : Lecture 20

Source material


Last modified: Sat Feb 27 14:50:56 IST 2016