Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution

DOI10.1007/978-3-319-41591-8_16zbMath1390.68181OpenAlexW2484748087MaRDI QIDQ4571133

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

Publication date: 6 July 2018

Published in: Software Engineering and Formal Methods (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution

Uses Software

• Yices
• z3

Cites Work

• Ranking function synthesis for bit-vector relations
• Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs
• Proving Termination of Programs Automatically with AProVE
• Proving Termination and Memory Safety for Programs with Pointer Arithmetic
• Linear Ranking for Linear Lasso Programs
• Termination Analysis of C Programs Using Compiler Intermediate Languages

This page was built for publication: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution