Proving termination and memory safety for programs with pointer arithmetic

DOI10.1007/978-3-319-08587-6_15MaRDI QIDQ3192191zbMATH OpenOpenAlexFDO

Authors Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten Fuhs, Jera Hensel, Peter Schneider-Kamp

Publication date 26 September 2014

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08587-6_15

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automatically proving termination and memory safety for programs with pointer arithmetic
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Automata-Based Termination Proofs
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps

Cited in

(7)

• Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic
• Proving termination of programs with bitvector arithmetic by symbolic execution
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
• Automata-Based Termination Proofs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Kruskal's tree theorem for acyclic term graphs

Describes a project that uses

Uses Software

• AProVE
• Vellvm

This page was built for publication: Proving termination and memory safety for programs with pointer arithmetic

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