Conference item icon

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:
Publisher copy:
10.1007/978-3-662-46669-8_27

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author

Contributors

Role:
Editor
Publisher:
Springer
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 More from this journal
Volume:
9032
Pages:
661-684
Publication date:
2015-01-01
DOI:
ISBN:
9783662466681
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


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP