Ultimate Taipan: Trace Abstraction and Abstract Interpretation - (Competition Contribution).

Ultimate Taipan is a software model checker for C programs. It is based on a CEGAR variant, trace abstraction﾿[7], where program abstractions, counterexample selection and abstraction refinement are based on automata. Ultimate Taipan constructs path programs from counterexamples and computes fixpoints for those path programs using abstract interpretation. If the fixpoints are strong enough to prove the path program to be correct, they are guaranteed to be loop invariants for the path program. If they are not strong enough, Ultimate Taipan uses an interpolating SMT solver to obtain state assertions from the original counterexample, thus guaranteeing progress.