Conference item
Propositional reasoning about safety and termination of heap-manipulating programs
- Abstract:
-
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 backgroun...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Accepted manuscript, pdf, 386.9KB)
-
- Publisher copy:
- 10.1007/978-3-662-46669-8_27
Bibliographic Details
- Publisher:
- Springer Publisher's website
- Host title:
- Lecture Notes in Computer Science: ESOP 2015: Programming Languages and Systems
- Journal:
- Lecture Notes in Computer Science: ESOP 2015: Programming Languages and Systems Journal website
- Volume:
- 9032
- Pages:
- 661-684
- Publication date:
- 2015-01-01
- DOI:
- ISBN:
- 9783662466681
Item Description
- Keywords:
- Pubs id:
-
pubs:576438
- UUID:
-
uuid:c7f5e5e9-42d9-4715-869d-16fff880c20d
- Local pid:
- pubs:576438
- Source identifiers:
-
576438
- Deposit date:
- 2017-01-28
Terms of use
- Copyright holder:
- Springer-Verlag Berlin Heidelberg
- Copyright date:
- 2015
- Notes:
- © Springer-Verlag Berlin Heidelberg 2015. This is the accepted manuscript version of the article. The final version is available online from Springer at: 10.1007/978-3-662-46669-8_27
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record