Paper Info
Title
Partial Orders for Efficient BMC of Concurrent Software
Abstract
The vast number of interleavings that a concurrent program can have is typically identified as the root cause of the difficulty of automatic analysis of concurrent software. Weak memory is generally believed to make this problem even harder. We address both issues by modelling programs' executions with partial orders rather than the interleaving semantics (SC). We implemented a software analysis tool based on these ideas. It scales to programs of sufficient size to achieve first-time formal verification of non-trivial concurrent systems code over a wide range of models, including SC, Intel x86 and IBM Power.
Year
Venue
Field
2013
CoRR
x86,IBM,Programming language,Software analysis pattern,Computer science,Parallel computing,Algorithm,Software,Interleaving semantics,Root cause,Formal verification
DocType
Volume
Citations 
Journal
abs/1301.1629
3
PageRank 
References 
Authors
0.43
28
3
Name
Order
Citations
PageRank
Jade Alglave160826.53
Daniel Kroening23084187.60
Michael Tautschnig342525.84