Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
From MaRDI portal
Publication:1647969
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
Analysis of algorithms and problem complexity (68Q25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
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