Analyzing program behavior through active automata learning.

The objective of the RERS Challenge 2013 was to analyze program behavior with respect to given sets of LTL and reachability properties for a set of reactive programs. The programs in various sizes and complexities could be divided into three different categories, depending on the available information: from black-box (binary-only) to white-box (full source code) over a mixed form thereof (grey-box). In this paper we present our approach to tackling the challenge problems, which is based on active automata learning. This required extending automata learning algorithms to exploit the given information, and adapting them in order to overcome problem-specific obstacles. We describe general optimizations and discuss the achieved results. [ABSTRACT FROM AUTHOR]