Paper Info
Title
Partial orders for efficient bounded model checking of concurrent software
Abstract
The number of interleavings of a concurrent program makes automatic analysis of such software very hard. Modern multiprocessors' execution models make this problem even harder. Modelling program executions with partial orders rather than interleavings addresses both issues: we obtain an efficient encoding into integer difference logic for bounded model checking that enables first-time formal verification of deployed concurrent systems code. We implemented the encoding in the CBMC tool and present experiments over a wide range of memory models, including SC, Intel x86 and IBM Power. Our experiments include core parts of PostgreSQL, the Linux kernel and the Apache HTTP server.
Year
DOI
Venue
2013
10.1007/978-3-642-39799-8_9
CAV
Field
DocType
Citations 
x86,Model checking,Programming language,Computer science,Theoretical computer science,Memory model,Linux kernel,Parallel computing,Algorithm,Web server,Bounded function,Encoding (memory),Formal verification
Conference
66
PageRank 
References 
Authors
1.81
34
3
Name
Order
Citations
PageRank
Jade Alglave160826.53
Daniel Kroening23084187.60
Michael Tautschnig342525.84