Propositional reasoning about safety and termination of heap-manipulating programs

DOI10.1007/978-3-662-46669-8_27MaRDI QIDQ2802460zbMATH OpenOpenAlexFDO

Authors Cristina David, Daniel Kroening, Matthew Lewis

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1410.5088

zbMATH Keywords

heapsafetySATtermination

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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 a background, 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 use it to check safety and termination proofs for several heap-manipulating programs.

Recommendations

• On Flat Programs with Lists
• Cyclic proofs of program termination in separation logic
• Modular reasoning about heap paths via effectively propositional formulas
• Verifying properties of well-founded linked lists
• Towards Model-Checking Programs with Lists

Cited in

(6)

• Cyclic proofs of program termination in separation logic
• Towards Model-Checking Programs with Lists
• Accurate invariant checking for programs manipulating lists and arrays with infinite data
• Verifying properties of well-founded linked lists
• On Flat Programs with Lists
• Proving Termination of C Programs with Lists

Describes a project that uses

Uses Software

• THOR

This page was built for publication: Propositional reasoning about safety and termination of heap-manipulating programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802460)