Proving Termination and Memory Safety for Programs with Pointer Arithmetic

DOI10.1007/978-3-319-08587-6_15zbMATH Open1423.68110OpenAlexW1788078288MaRDI QIDQ3192191FDOQ3192191

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

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)

Cited In (5)

• Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Title not available (Why is that?)
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic

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)