January 2014 - tr-announce - lists.rwth-aachen.de

2014-05: Automated Termination Analysis for Programs with Pointer Arithmetic
by Thomas Ströder 01 Feb '14

01 Feb '14

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.

1 0

2014-04: Languages of Infinite Traces and Deterministic Asynchronous Automata
by Thomas Ströder 31 Jan '14

31 Jan '14

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.

1 0

2013-19: Support for error tolerance in the Real-Time Transport Protocol
by Thomas Ströder 08 Jan '14

08 Jan '14

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%.

1 0