Propositional reasoning about safety and termination of heap-manipulating programs
This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. For this purpose, we p...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2015
|
| _version_ | 1797094251543134208 |
|---|---|
| author | David, C Kroening, D Lewis, M |
| author2 | Vitek, J |
| author_facet | Vitek, J David, C Kroening, D Lewis, M |
| author_sort | David, C |
| collection | OXFORD |
| description | This paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. For this purpose, we propose the theory SLH of singly-linked lists with length, which is able to capture non-trivial interactions between shape and arithmetic. When using the theory of bit-vector arithmetic as background theory, SLH is efficiently decidable via a reduction to SAT. We show the utility of SLH for software verification by using it to express safety invariants and termination arguments for programs manipulating potentially cyclic, singly-linked lists with unrestricted, unspecified sharing. We also provide an implementation of the decision procedure and apply it to check safety and termination proofs for several heap-manipulating programs. |
| first_indexed | 2024-03-07T04:11:28Z |
| format | Conference item |
| id | oxford-uuid:c7f5e5e9-42d9-4715-869d-16fff880c20d |
| institution | University of Oxford |
| last_indexed | 2024-03-07T04:11:28Z |
| publishDate | 2015 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:c7f5e5e9-42d9-4715-869d-16fff880c20d2022-03-27T06:49:02ZPropositional reasoning about safety and termination of heap-manipulating programsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:c7f5e5e9-42d9-4715-869d-16fff880c20dSymplectic Elements at OxfordSpringer2015David, CKroening, DLewis, MVitek, JThis paper shows that it is possible to reason about the safety and termination of programs handling potentially cyclic, singly-linked lists using propositional reasoning even when the safety invariants and termination arguments depend on constraints over the lengths of lists. For this purpose, we propose the theory SLH of singly-linked lists with length, which is able to capture non-trivial interactions between shape and arithmetic. When using the theory of bit-vector arithmetic as background theory, SLH is efficiently decidable via a reduction to SAT. We show the utility of SLH for software verification by using it to express safety invariants and termination arguments for programs manipulating potentially cyclic, singly-linked lists with unrestricted, unspecified sharing. We also provide an implementation of the decision procedure and apply it to check safety and termination proofs for several heap-manipulating programs. |
| spellingShingle | David, C Kroening, D Lewis, M Propositional reasoning about safety and termination of heap-manipulating programs |
| title | Propositional reasoning about safety and termination of heap-manipulating programs |
| title_full | Propositional reasoning about safety and termination of heap-manipulating programs |
| title_fullStr | Propositional reasoning about safety and termination of heap-manipulating programs |
| title_full_unstemmed | Propositional reasoning about safety and termination of heap-manipulating programs |
| title_short | Propositional reasoning about safety and termination of heap-manipulating programs |
| title_sort | propositional reasoning about safety and termination of heap manipulating programs |
| work_keys_str_mv | AT davidc propositionalreasoningaboutsafetyandterminationofheapmanipulatingprograms AT kroeningd propositionalreasoningaboutsafetyandterminationofheapmanipulatingprograms AT lewism propositionalreasoningaboutsafetyandterminationofheapmanipulatingprograms |