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

We introduce Ultimate TestGen, a novel tool for automatic test-case generation. Like many other test-case generators, Ultimate Test-Gen 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.