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: |