Heizmann, Matthias; Dietsch, Daniel; Leike, Jan; Musa, Betim; Podelski, Andreas
Ultimate Automizer is a software verification tool that is able to analyze reachability of an error label, memory safety, and termination of C programs. For all three tasks, our tool follows an automatabased approach where interpolation is used to compute proofs for traces. The interpolants are generated via a new scheme that requires only the post operator, unsatisfiable cores and live variable analysis. This new scheme enables our tool to use the SMT theory of arrays in combination with...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.