Automatically proving termination and memory safety for programs with pointer arithmetic

DOI10.1007/s10817-016-9389-xzbMath1409.68077OpenAlexW2536541088MaRDI QIDQ2362494

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

Publication date: 10 July 2017

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://eprints.bbk.ac.uk/id/eprint/16552/1/JAR-llvm-pointer.pdf

zbMATH Keywords

terminationsymbolic executionmemory safetyLLVMC programs

Mathematics Subject Classification ID

Related Items (2)

Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution ⋮ Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free

Uses Software

• Coq
• Isabelle/HOL
• Yices
• z3
• LLVM
• KLEE
• ARMC
• CeTA
• CPAchecker
• AProVE
• LLBMC
• UFO
• SLAyer
• CoLoR
• CiME
• Ctrl
• KITTeL
• Verasco
• Infer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programs with lists are counter automata
• Modular inference of subprogram contracts for safety checking
• Precise interprocedural dataflow analysis with applications to constant propagation
• Cost analysis of object-oriented bytecode programs
• Summarization for termination: No return!
• The octagon abstract domain
• Isabelle/HOL. A proof assistant for higher-order logic
• Conflict-driven conditional termination
• Lower bounds for runtime complexity of term rewriting
• Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
• Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs
• Formalizing the LLVM intermediate representation for verified program transformations
• Loop Summarization and Termination Analysis
• Termination Graphs for Java Bytecode
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
• Certification of Termination Proofs Using CeTA
• Variance analyses from invariance analyses
• Proving Termination of Programs Automatically with AProVE
• Proving Termination and Memory Safety for Programs with Pointer Arithmetic
• Proving Termination Through Conditional Termination
• Counterexample-guided abstraction refinement for symbolic model checking
• Solving SAT and SAT Modulo Theories
• Constrained Term Rewriting tooL
• Proving Termination of Tree Manipulating Programs
• Efficient E-Matching for SMT Solvers
• Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
• Proving Termination of Integer Term Rewriting
• Automata-Based Termination Proofs
• Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
• Alternation for Termination
• Linear Ranking for Linear Lasso Programs
• Automatic numeric abstractions for heap-manipulating programs
• Termination Analysis of C Programs Using Compiler Intermediate Languages
• Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
• Automated Termination Analysis of Java Bytecode by Term Rewriting
• An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
• A Certified Denotational Abstract Interpreter
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Static Analysis

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