2015 | OriginalPaper | Buchkapitel
ULTIMATE KOJAK with Memory Safety Checks
(Competition Contribution)
verfasst von : Alexander Nutz, Daniel Dietsch, Mostafa Mahmoud Mohamed, Andreas Podelski
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Ultimate Kojak
is a symbolic software model checker implemented in the
Ultimate
framework. It follows the CEGAR approach and uses Craig interpolants to refine an overapproximation of the program until it can either prove safety or has found a real counterexample.
This year’s version features a new refinement algorithm, a precise treatment of heap memory, which allows us to deal with pointer aliasing and to participate in the memsafety category, and an improved interpolants generator.