Proving Termination and Memory Safety for Programs with Pointer Arithmetic

DOI10.1007/978-3-319-08587-6_15zbMath1423.68110OpenAlexW1788078288MaRDI QIDQ3192191

Marc Brockschmidt, Jürgen Giesl, Thomas Ströder, Carsten Fuhs, Jera Hensel, Florian Frohn, 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

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

Related Items (4)

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution ⋮ Unnamed Item

Uses Software

• AProVE
• Vellvm

This page was built for publication: Proving Termination and Memory Safety for Programs with Pointer Arithmetic