Conference item
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.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 366.6KB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-642-39799-8_9
- Publisher:
- Springer
- Host title:
- Lecture Notes in Computer Science: CAV 2013: Computer Aided Verification
- Journal:
- Lecture Notes in Computer Science: CAV 2013: Computer Aided Verification More from this journal
- Volume:
- 8044
- Pages:
- 141-157
- Publication date:
- 2013-08-12
- DOI:
- ISSN:
-
0302-9743 and 1611-3349
- ISBN:
- 9783642397981
- Keywords:
- Pubs id:
-
pubs:418033
- UUID:
-
uuid:b3531391-c4b4-4c38-a279-1799dedb1f1c
- Local pid:
-
pubs:418033
- Source identifiers:
-
418033
- Deposit date:
-
2017-01-28
Terms of use
- Copyright holder:
- Springer-Verlag Berlin Heidelberg
- Copyright date:
- 2013
- Notes:
- © Springer-Verlag Berlin Heidelberg 2013. This is the accepted manuscript version of the article. The final version is available online from Springer at: 10.1007/978-3-642-39799-8_9
If you are the owner of this record, you can report an update to it here: Report update to this record