Partial orders for efficient bounded model checking of concurrent software
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 en...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2013
|
| _version_ | 1797089733095981056 |
|---|---|
| author | Alglave, J Kroening, D Tautschnig, M |
| author2 | Sharygina, N |
| author_facet | Sharygina, N Alglave, J Kroening, D Tautschnig, M |
| author_sort | Alglave, J |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-07T03:08:18Z |
| format | Conference item |
| id | oxford-uuid:b3531391-c4b4-4c38-a279-1799dedb1f1c |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:08:18Z |
| publishDate | 2013 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:b3531391-c4b4-4c38-a279-1799dedb1f1c2022-03-27T04:18:10ZPartial orders for efficient bounded model checking of concurrent softwareConference itemhttp://purl.org/coar/resource_type/c_5794uuid:b3531391-c4b4-4c38-a279-1799dedb1f1cSymplectic Elements at OxfordSpringer2013Alglave, JKroening, DTautschnig, MSharygina, NVeith, HThe 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. |
| spellingShingle | Alglave, J Kroening, D Tautschnig, M Partial orders for efficient bounded model checking of concurrent software |
| title | Partial orders for efficient bounded model checking of concurrent software |
| title_full | Partial orders for efficient bounded model checking of concurrent software |
| title_fullStr | Partial orders for efficient bounded model checking of concurrent software |
| title_full_unstemmed | Partial orders for efficient bounded model checking of concurrent software |
| title_short | Partial orders for efficient bounded model checking of concurrent software |
| title_sort | partial orders for efficient bounded model checking of concurrent software |
| work_keys_str_mv | AT alglavej partialordersforefficientboundedmodelcheckingofconcurrentsoftware AT kroeningd partialordersforefficientboundedmodelcheckingofconcurrentsoftware AT tautschnigm partialordersforefficientboundedmodelcheckingofconcurrentsoftware |