The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Automated Termination Analysis for Programs with Pointer Arithmetic
Thomas Ströder, Jürgen Giesl, Marc Brockschmidt, Florian Frohn, Carsten
Fuhs, Jera Hensel, and Peter Schneider-Kamp
AIB 2014-05
While automated verification of imperative programs was studied
intensively, proving termination of programs with explicit pointer
arithmetic is still an open problem. To close this gap, we introduce a
novel abstract domain that can track allocated memory in detail. We use
it to automatically construct a symbolic execution graph that represents
all possible runs of the program. This graph is then transformed into an
integer transition system, whose termination can be proved by standard
techniques. We implemented this approach in the automated termination
prover AProVE and demonstrate its capability of analyzing C programs
with pointer arithmetic that existing tools cannot handle.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Languages of Infinite Traces and Deterministic Asynchronous Automata
Namit Chaturvedi
AIB 2014-04
In the theory of deterministic automata for languages of infinite words,
a fundamental fact relates the family of infinitary limits of regular
languages and the family of omega-languages recognized by deterministic
Buechi automata. With the known definitions of asynchronous automata,
this observation does not extend to the context of traces. A major
difficulty is posed by processes that stall after finitely many
transitions. We introduce the family of deterministic,
synchronization-aware asynchronous automata which -- using as parameter
the set of processes that stay live ad infinitum -- allows us to settle
an open question, namely, whether there exists a deterministic Buechi
automaton recognizing precisely the infinitary limit of a regular trace
language. Also, the corresponding class of unparameterized Muller
automata captures all omega-Regular trace languages.
The following technical report is available from
http://aib.informatik.rwth-aachen.de:
Support for error tolerance in the Real-Time Transport Protocol
Florian Schmidt, David Orlea, and Klaus Wehrle
AIB 2013-19
Streaming applications often tolerate bit errors in their received data
well. This is contrasted by the enforcement of correctness of the packet
headers and payload by network protocols. We investigate a solution for
the Real-time Transport Protocol (RTP) that is tolerant to errors by
accepting erroneous data. It passes potentially corrupted stream data
payloads to the codecs. If errors occur in the header, our solution
recovers from these by leveraging the known state and expected header
values for each stream. The solution is fully receiver-based and
incrementally deployable, and as such requires neither support from the
sender nor changes to the RTP specification. Evaluations show that our
header error recovery scheme can recover from almost all errors, with
virtually no erroneous recoveries, up to bit error rates of about 10%.