Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution

DOI10.1016/j.jlamp.2018.02.004zbMath1395.68093OpenAlexW2792248360MaRDI QIDQ1647969

Jürgen Giesl, Jera Hensel, Florian Frohn, Thomas Ströder

Publication date: 27 June 2018

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2018.02.004

zbMATH Keywords

runtime complexitysymbolic executiontermination analysis\textsf{LLVM}bitvectors

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Yices
• z3
• LLVM
• AProVE
• ABC
• KITTeL

Cites Work

• Cost analysis of object-oriented bytecode programs
• Ranking function synthesis for bit-vector relations
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Resource Analysis of Complex Programs with Cost Equations
• Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs
• ABC: Algebraic Bound Computation for Loops
• SPEED: Symbolic Complexity Bound Analysis
• Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
• Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
• Linear Ranking for Linear Lasso Programs
• Towards automatic resource bound analysis for OCaml
• Termination Analysis of C Programs Using Compiler Intermediate Languages