3.00 p.m.
Verification of concurrent C programs with an unbounded number of threads
Daniel Kroening
Computer Science Department, University of Oxford.
08-01-13

---

Abstract

Concurrency is gaining importance due to the trend towards multi-core architectures, even in resource-constrained environments. I will present a technique to abstract concurrent C programs into a Boolean program in a way that preserves the symmetry present in the system. Assertion checking in the C program then corresponds to coverability checking on the Boolean program. The coverability problem is solved with a novel analysis engine that combines forward and backward search. The talk summarises papers that have appeared at CAV 2009, 2010, 2011 and CONCUR 2012.