The goal of this project is to develop algorithms and tools for automated formal verification of low-level C programs that make use of shared-variable concurrency. In spite of extensive research on concurrent computation, almost all existing program analysis tools are limited to sequential programs or programs that communicate via some form of explicit message passing. However, shared-variable concurrency is the predominant form of concurrency in commercial environments, and tool support is in dire need. The project focuses on
- verification by means of automated summarisation of threads,
- identification of transactions, enabling partial-order reductions, and
- Craig interpolation to derive thread invariants.
