Abstract
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.
Cite
CITATION STYLE
Greitschus, M., Dietsch, D., Heizmann, M., Nutz, A., Schätzle, C., Schilling, C., … Podelski, A. (2017). Ultimate taipan: Trace abstraction and abstract interpretation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10206 LNCS, pp. 399–403). Springer Verlag. https://doi.org/10.1007/978-3-662-54580-5_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
