Proving Termination of C Programs with Lists

DOI10.1007/978-3-031-38499-8_16MaRDI QIDQ6492749zbMATH OpenFDO

Authors Jera Hensel, Jürgen Giesl

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_16

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automated termination analysis of Java bytecode by term rewriting
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Formalizing the LLVM intermediate representation for verified program transformations
• Modular termination proofs of recursive Java bytecode programs by term rewriting
• Propositional reasoning about safety and termination of heap-manipulating programs
• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Quantitative separation logic and programs with lists
• Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution

Cited in

(1)

• Automatic bit- and memory-precise verification of eBPF code

This page was built for publication: Proving Termination of C Programs with Lists

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