Proving termination and memory safety for programs with pointer arithmetic
DOI10.1007/978-3-319-08587-6_15zbMATH Open1423.68110OpenAlexW1788078288MaRDI QIDQ3192191FDOQ3192191
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
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
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 (7)
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automata-Based Termination Proofs
- Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
- Proving termination of programs with bitvector arithmetic by symbolic execution
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic
- Kruskal's tree theorem for acyclic term graphs
Uses Software
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)
