3.30 pm, Lecture Hall 1
A Short Course on Algorithmic Program Verification
IRIF, Univ. of Paris-Diderot, France.
TITLE : A Short Course on Algorithmic Program Verification
Speaker: Ahmed Bouajjani, IRIF, Univ. of Paris-Diderot, France
Venue : Lecture Hall 804 (9th February 2017) / Seminar Hall (14th, 16th and 21st February, 2017), CMI
Time and Date: 3.30pm on 9th, 14th, 16th and 21st February, 2017 (Tuesdays/Thursdays).
The four lectures address the issue of verifying automatically the correctness of programs. This is a challenging problem due to several sources of complexity. Besides the fact that programs manipulate in general data ranging over infinite domains, programs may also have complex control structures due to, e.g., recursive procedure calls, concurrency, dynamic creation of threads, etc. In fact, even when program variables are over finite domains (such as booleans), aspects such as recursion and concurrency make program verification extremely hard, beyond the scope of classical model-checking techniques for finite-state systems. The lectures focus on these aspects and explore the decidability limits and the complexity of verification problems (mainly reachability problems) for various importants classes of programs.
Only familiarity with basic concepts in automata theory (finite automata, pushdown automata and decidability) will be assumed.
The four lectures will cover (if time permits) the following topics: - sequential programs with recursive procedures calls: modelling using pushdown systems, automata-based reachability analysis. - concurrent programs with dynamic creation of processes/tasks: modelling using Petri nets, reduction to the coverability problem. - concurrent programs with recursive procedure calls: undecidability in the general case, relevant assumptions/restrictions are needed. - a particular class of programs: event-driven asynchronous programs. Modelling with pushdown systems + multisets. Decidability and complexity. Reduction to coverability in Petri nets using task summary computations. - under-approximate analysis: context-bounded analysis. Decidability and complexity. Verification based on sequentialisation. - libraries implementing concurrent abstract objects (such as concurrent stacks, queues, etc.). Observational refinement vs linearizability. - Verifying linearizability: Decidability and complexity. Tractable reductions to state reachability problems.