Sciweavers

CORR
2010
Springer

Bounded Model Checking of Multi-threaded Software using SMT solvers

13 years 10 months ago
Bounded Model Checking of Multi-threaded Software using SMT solvers
The transition from single-core to multi-core processors has made multi-threaded software an important subject in computer aided verification. Here, we describe and evaluate an extension of the ESBMC model checker to support the verification of multi-threaded software with shared variables and locks using bounded model checking (BMC) based on Satisfiability Modulo Theories (SMT). We describe three approaches to model check multi-threaded software and our modelling of the synchronization primitives of the Pthread library. In the lazy approach, we generate all possible interleavings and call the BMC procedure on each of them individually, until we either find a bug, or have systematically explored all interleavings. In the schedule recording approach, we encode all possible interleavings into one single formula and then exploit the high speed of the SMT solvers. In the underapproximation-widening approach, we he state space by abstracting the number of state variables and interleavings ...
Lucas Cordeiro, Bernd Fischer 0002
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2010
Where CORR
Authors Lucas Cordeiro, Bernd Fischer 0002
Comments (0)