Verifying multi-threaded software with impact
Lazy abstraction with interpolants, also known as the Impact algorithm, is en vogue as a state-of-the-art software model-checking technique for sequential programs. However, a direct extension of the Impact algorithm to concurrent programs is bound to be inefficient as it has to explore all thread i...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
IEEE
2013
|
| _version_ | 1797064351858819072 |
|---|---|
| author | Wachter, B Kroening, D Ouaknine, J |
| author_facet | Wachter, B Kroening, D Ouaknine, J |
| author_sort | Wachter, B |
| collection | OXFORD |
| description | Lazy abstraction with interpolants, also known as the Impact algorithm, is en vogue as a state-of-the-art software model-checking technique for sequential programs. However, a direct extension of the Impact algorithm to concurrent programs is bound to be inefficient as it has to explore all thread interleavings, which leads to control-state explosion. To this end, we present a new algorithm that combines a new, symbolic form of partial-order reduction with Impact. Our algorithm carries out the dependence analysis on-the-fly while constructing the abstraction and is thus able to deal precisely with dynamic dependencies arising from accesses to tables or pointers - a setting where classical static partial-order reduction techniques struggle. We have implemented the algorithm in a prototype tool that analyses concurrent C program with POSIX threads and evaluated it on a number of benchmark programs. To our knowledge, this is the first application of an Impact-like algorithm to concurrent programs. |
| first_indexed | 2024-03-06T21:13:02Z |
| format | Conference item |
| id | oxford-uuid:3ed3c72c-0a7d-4b71-a7ef-00d46e139a62 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T21:13:02Z |
| publishDate | 2013 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:3ed3c72c-0a7d-4b71-a7ef-00d46e139a622022-03-26T14:28:00ZVerifying multi-threaded software with impactConference itemhttp://purl.org/coar/resource_type/c_5794uuid:3ed3c72c-0a7d-4b71-a7ef-00d46e139a62Symplectic Elements at OxfordIEEE2013Wachter, BKroening, DOuaknine, JLazy abstraction with interpolants, also known as the Impact algorithm, is en vogue as a state-of-the-art software model-checking technique for sequential programs. However, a direct extension of the Impact algorithm to concurrent programs is bound to be inefficient as it has to explore all thread interleavings, which leads to control-state explosion. To this end, we present a new algorithm that combines a new, symbolic form of partial-order reduction with Impact. Our algorithm carries out the dependence analysis on-the-fly while constructing the abstraction and is thus able to deal precisely with dynamic dependencies arising from accesses to tables or pointers - a setting where classical static partial-order reduction techniques struggle. We have implemented the algorithm in a prototype tool that analyses concurrent C program with POSIX threads and evaluated it on a number of benchmark programs. To our knowledge, this is the first application of an Impact-like algorithm to concurrent programs. |
| spellingShingle | Wachter, B Kroening, D Ouaknine, J Verifying multi-threaded software with impact |
| title | Verifying multi-threaded software with impact |
| title_full | Verifying multi-threaded software with impact |
| title_fullStr | Verifying multi-threaded software with impact |
| title_full_unstemmed | Verifying multi-threaded software with impact |
| title_short | Verifying multi-threaded software with impact |
| title_sort | verifying multi threaded software with impact |
| work_keys_str_mv | AT wachterb verifyingmultithreadedsoftwarewithimpact AT kroeningd verifyingmultithreadedsoftwarewithimpact AT ouakninej verifyingmultithreadedsoftwarewithimpact |