FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Complexity Analysis for Bitvector Programs

Authors: Jera Hensel, Florian Frohn and Jürgen Giesl

Paper Information

Title:Complexity Analysis for Bitvector Programs
Authors:Jera Hensel, Florian Frohn and Jürgen Giesl
Proceedings:WST WST2018proceedings
Editor: Salvador Lucas
Keywords:Complexity Analysis, Bitvectors, C Programming Language, Integer Transition Systems
Abstract:

ABSTRACT. In earlier work, we developed approaches for automated termination analysis of several different programming languages, based on back-end techniques for termination proofs of term rewrite systems and integer transition systems. In the last years, we started adapting these approaches in order to analyze the complexity of programs as well. However, up to now a severe drawback was that we assumed the program variables to range over mathematical integers instead of bitvectors. This eases mathematical reasoning but is unsound in general. While we recently showed how to handle fixed-width bitvector integers in termination analysis, we now present the first technique to analyze the runtime complexity of programs with bitvector arithmetic. We implemented our contributions in the tool AProVE and evaluate its power by extensive experiments.

Pages:1
Talk:Jul 19 11:00 (Session 132J: Complexity)
Paper: