Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
type: Item
instance of: scholarly article
title: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution
zbMATH Open document ID: 1395.68093
author: Jera Hensel
author: Jürgen Giesl
author: Florian Frohn
author: Thomas Ströder
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2018-06-27T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 6894965
zbMATH Keywords: termination analysis
zbMATH Keywords: bitvectors
zbMATH Keywords: symbolic execution
zbMATH Keywords: \textsf{LLVM}
zbMATH Keywords: runtime complexity
describes a project that uses: AProVE
describes a project that uses: Yices
describes a project that uses: z3
describes a project that uses: LLVM
describes a project that uses: KITTeL
describes a project that uses: ABC
MaRDI profile type: Publication
full work available at URL: j.jlamp.2018.02.004
OpenAlex ID: W2792248360
cites work: Cost analysis of object-oriented bytecode programs
cites work: Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
cites work: ABC: Algebraic Bound Computation for Loops
cites work: Ranking function synthesis for bit-vector relations
cites work: Unrestricted Termination and Non-termination Arguments for Bit-Vector Programs
cites work: Termination Analysis of C Programs Using Compiler Intermediate Languages
cites work: Resource Analysis of Complex Programs with Cost Equations
cites work: Analyzing program termination and complexity automatically with \textsf{AProVE}
cites work: SPEED: Symbolic Complexity Bound Analysis
cites work: Linear Ranking for Linear Lasso Programs
cites work: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
cites work: Towards automatic resource bound analysis for OCaml
cites work: Automatically proving termination and memory safety for programs with pointer arithmetic
Wikidata QID: Q130156793
DOI: 10.1016/J.JLAMP.2018.02.004
description: scientific article; zbMATH DE number 6894965