Ultimate TestGen: Test-Case Generation with Automata-based Software Model Checking (Competition Contribution).

AbstractWe introduce Ultimate TestGen, a novel tool for automatic test-case generation. Like many other test-case generators, Ultimate TestGen builds on verification technology, i.e., it checks the (un)reachability of test goals and generates test cases from counterexamples. In contrast to existing tools, it applies trace abstraction, an automata-theoretic approach to software model checking, which is implemented in the successful verifier Ultimate Automizer. To avoid that the same test goal is reached again, Ultimate TestGen extends the automata-theoretic model checking approach with error automata.