Ultimate Automizer is a software verifier that implements an automata-theoretic verification approach. The tool is able to check non-reachability, memory safety, the absence of overflows, and termination. The input are sequential and concurrent program that are written in the C language. The verification approach is based on a new view to programs. In this new view, the focus lies not on program states, instead the focus lies on sequences of statements, which we call traces. We view a program as an automaton whose alphabet consists of the program’s statements. Hence, each program defines a set of traces and we can apply automata-theoretic operations to programs. Ultimate Automizer uses this connection between programs and sets of traces to decompose a program, to prove correctness of the components, and to compose these correctness proofs to a correctness proof for the program.