Verification of Shared-Memory Concurrent Software
1st March 2010 to 31st August 2013
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.
Sponsors
Principal Investigator
People
Share this:
