tr-announce April 2016

tr-announce@lists.rwth-aachen.de

1 participants
2 discussions

2016-04: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution

by Jera Hensel

The following technical report is available from http://aib.informatik.rwth-aachen.de: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution Jera Hensel, Jürgen Giesl, Florian Frohn, and Thomas Ströder AIB 2016-04 In earlier work, we developed an approach for automated termination analysis of C programs with explicit pointer arithmetic, which is based on symbolic execution. However, similar to many other termination techniques, this approach assumed the program variables to range over mathematical integers instead of bitvectors. This eases mathematical reasoning but is unsound in general. In this paper, we extend our approach in order to handle fixed-width bitvector integers. Thus, we present the first technique for termination analysis of C programs that covers both byte-accurate pointer arithmetic and bit-precise modeling of integers. We implemented our approach in the automated termination prover AProVE and evaluate its power by extensive experiments.

8 years, 4 months

2016-03: Lower Runtime Bounds for Integer Programs

by Jera Hensel

The following technical report is available from http://aib.informatik.rwth-aachen.de: Lower Runtime Bounds for Integer Programs Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, and Jürgen Giesl AIB 2016-03 We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs. To this end, we construct symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large number of examples.

8 years, 5 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce April 2016