Abstract
Ultimate Automizer is a software verifier that generalizes proofs for traces to proofs for larger parts for the program. In recent years the portfolio of proof producers that are available to Ultimate has grown continuously. This is not only because more trace analysis algorithms have been implemented in Ultimate but also due to the continuous progress in the SMT community. In this paper we explain how Ultimate Automizer dynamically selects trace analysis algorithms and how the tool decides when proofs for traces are “good” enough for using them in the abstraction refinement.
Cite
CITATION STYLE
Heizmann, M., Chen, Y. F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., … Podelski, A. (2018). Ultimate automizer and the search for perfect interpolants: (Competition contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10806 LNCS, pp. 447–451). Springer Verlag. https://doi.org/10.1007/978-3-319-89963-3_30
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
