Efficient coverability analysis by proof minimization
We consider multi-threaded programs with an unbounded number of threads executing a finite-state, non-recursive procedure. Safety properties of such programs can be checked via reduction to the coverability problem for well-structured transition systems (WSTS). In this paper, we present a novel, sou...
| Autori principali: | , , |
|---|---|
| Altri autori: | |
| Natura: | Conference item |
| Pubblicazione: |
Springer
2012
|
| _version_ | 1826274317320585216 |
|---|---|
| author | Kaiser, A Kroening, D Wahl, T |
| author2 | Koutny, M |
| author_facet | Koutny, M Kaiser, A Kroening, D Wahl, T |
| author_sort | Kaiser, A |
| collection | OXFORD |
| description | We consider multi-threaded programs with an unbounded number of threads executing a finite-state, non-recursive procedure. Safety properties of such programs can be checked via reduction to the coverability problem for well-structured transition systems (WSTS). In this paper, we present a novel, sound and complete yet empirically much improved solution to this problem. The key idea to achieve a compact search structure is to track uncoverability only for minimal uncoverable elements, even if these elements are not part of the original coverability query. To this end, our algorithm examines elements in the downward closure of elements backward-reachable from the initial queries. A downside is that the algorithm may unnecessarily explore elements that turn out coverable and thus fail to contribute to the proof minimization. We counter this effect using a forward search engine that simultaneously generates (a subset of all) coverable elements, e.g., a generalized Karp-Miller procedure. We demonstrate in extensive experiments on C programs that our approach targeting minimal uncoverability proofs outperforms existing techniques by orders of magnitude. |
| first_indexed | 2024-03-06T22:41:36Z |
| format | Conference item |
| id | oxford-uuid:5bc50a09-d27b-4da4-bf51-515d17c3e2aa |
| institution | University of Oxford |
| last_indexed | 2024-03-06T22:41:36Z |
| publishDate | 2012 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:5bc50a09-d27b-4da4-bf51-515d17c3e2aa2022-03-26T17:23:57ZEfficient coverability analysis by proof minimizationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:5bc50a09-d27b-4da4-bf51-515d17c3e2aaSymplectic Elements at OxfordSpringer2012Kaiser, AKroening, DWahl, TKoutny, MUlidowski, IWe consider multi-threaded programs with an unbounded number of threads executing a finite-state, non-recursive procedure. Safety properties of such programs can be checked via reduction to the coverability problem for well-structured transition systems (WSTS). In this paper, we present a novel, sound and complete yet empirically much improved solution to this problem. The key idea to achieve a compact search structure is to track uncoverability only for minimal uncoverable elements, even if these elements are not part of the original coverability query. To this end, our algorithm examines elements in the downward closure of elements backward-reachable from the initial queries. A downside is that the algorithm may unnecessarily explore elements that turn out coverable and thus fail to contribute to the proof minimization. We counter this effect using a forward search engine that simultaneously generates (a subset of all) coverable elements, e.g., a generalized Karp-Miller procedure. We demonstrate in extensive experiments on C programs that our approach targeting minimal uncoverability proofs outperforms existing techniques by orders of magnitude. |
| spellingShingle | Kaiser, A Kroening, D Wahl, T Efficient coverability analysis by proof minimization |
| title | Efficient coverability analysis by proof minimization |
| title_full | Efficient coverability analysis by proof minimization |
| title_fullStr | Efficient coverability analysis by proof minimization |
| title_full_unstemmed | Efficient coverability analysis by proof minimization |
| title_short | Efficient coverability analysis by proof minimization |
| title_sort | efficient coverability analysis by proof minimization |
| work_keys_str_mv | AT kaisera efficientcoverabilityanalysisbyproofminimization AT kroeningd efficientcoverabilityanalysisbyproofminimization AT wahlt efficientcoverabilityanalysisbyproofminimization |