Verification of Boolean programs with unbounded thread creation.
Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN 00, in: Lecture Notes in Computer Science, vol...
| Huvudupphovsmän: | , , |
|---|---|
| Materialtyp: | Journal article |
| Språk: | English |
| Publicerad: |
2007
|
| _version_ | 1826284673450377216 |
|---|---|
| author | Cook, B Kroening, D Sharygina, N |
| author_facet | Cook, B Kroening, D Sharygina, N |
| author_sort | Cook, B |
| collection | OXFORD |
| description | Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN 00, in: Lecture Notes in Computer Science, vol. 1885, Springer, 2000, pp. 113-130] are the most popular representation for these abstractions. Unfortunately, today's symbolic software model checkers are limited to the analysis of sequential programs due to the fact that reachability in Boolean programs with unbounded thread creation is undecidable. We address this limitation with a novel algorithm for over-approximating reachability in Boolean programs with unbounded thread creation. Although the Boolean programs are not of finite state, the algorithm always reaches a fix-point. The fixed points are detected by projecting the state of the threads to the globally visible parts, which are finite. © 2007 Elsevier Ltd. All rights reserved. |
| first_indexed | 2024-03-07T01:17:22Z |
| format | Journal article |
| id | oxford-uuid:8f25e1b6-2e9f-4522-b746-21438f5d652f |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T01:17:22Z |
| publishDate | 2007 |
| record_format | dspace |
| spelling | oxford-uuid:8f25e1b6-2e9f-4522-b746-21438f5d652f2022-03-26T23:02:25ZVerification of Boolean programs with unbounded thread creation.Journal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:8f25e1b6-2e9f-4522-b746-21438f5d652fEnglishSymplectic Elements at Oxford2007Cook, BKroening, DSharygina, NMost symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN 00, in: Lecture Notes in Computer Science, vol. 1885, Springer, 2000, pp. 113-130] are the most popular representation for these abstractions. Unfortunately, today's symbolic software model checkers are limited to the analysis of sequential programs due to the fact that reachability in Boolean programs with unbounded thread creation is undecidable. We address this limitation with a novel algorithm for over-approximating reachability in Boolean programs with unbounded thread creation. Although the Boolean programs are not of finite state, the algorithm always reaches a fix-point. The fixed points are detected by projecting the state of the threads to the globally visible parts, which are finite. © 2007 Elsevier Ltd. All rights reserved. |
| spellingShingle | Cook, B Kroening, D Sharygina, N Verification of Boolean programs with unbounded thread creation. |
| title | Verification of Boolean programs with unbounded thread creation. |
| title_full | Verification of Boolean programs with unbounded thread creation. |
| title_fullStr | Verification of Boolean programs with unbounded thread creation. |
| title_full_unstemmed | Verification of Boolean programs with unbounded thread creation. |
| title_short | Verification of Boolean programs with unbounded thread creation. |
| title_sort | verification of boolean programs with unbounded thread creation |
| work_keys_str_mv | AT cookb verificationofbooleanprogramswithunboundedthreadcreation AT kroeningd verificationofbooleanprogramswithunboundedthreadcreation AT sharyginan verificationofbooleanprogramswithunboundedthreadcreation |