On BMC Sequentializations of Concurrent Programs

Sequentialization is a technique for the analysis of concurrent programs that exploits mature verification techniques and tools that were originally designed for sequential programs.  It can be implemented as a code-to-code translation from the concurrent program into a corresponding non-deterministic sequential program that simulates all the targeted executions of the original program.  The sequential program contains both the mapping of the threads in the form of functions, and an encoding of the scheduler, where non-determinism is used to capture thread interleavings.  This approach has three main advantages: (1) a code-to-code translation is typically much easier to implement than a full-fledged analysis tool; (2) it allows designers to focus only on the concurrency aspects of programs, delegating all sequential reasoning  to an existing target analysis tool; (3) sequentializations can be designed to target multiple backends for sequential program analysis.  I will describe the design and the implementation of two sequentialization schemes targeted at using BMC tools as backends: Lazy and Memory-Unwinding sequentializations.  Our code-to-code translations are carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so that they produce tight SAT/SMT formulae, and are thus very effective in practice.

Speaker biography

Gennaro Parlato is a Lecturer in Automated Verification in the School of Electronics and Computer Science at the University of Southampton (UoS) and a member of the Academic Centre of Excellence in Cybersecurity Southampton.  Prior to joining UoS in 2011, he was a research associate in the Department of Computer Science at the University of Illinois at Urbana-Champaign, and a CNRS postdoc research associate in the Modeling and Verification research group at LIAFA laboratory in Paris.  He obtained his PhD in Computer Science at the University of Salerno in 2006.  Gennaro is interested in software verification and in building reliable and secure software systems using formal correctness techniques.