Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Predicate Analysis with Block-Abstraction Memoization
verfasst von : Daniel Wonisch, Heike Wehrheim
Erschienen in: Formal Methods and Software Engineering
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
Predicate abstraction is an established technique for reducing the size of the state space during verification. In this paper, we extend predication abstraction with
block-abstraction memoization
(BAM), which exploits the fact that blocks are often executed several times in a program. The verification can thus benefit from
caching
the values of previous block analyses and reusing them upon next entry into a block. In addition to function bodies, BAM also performs well for
nested loops
. To further increase effectiveness, block memoization has been integrated with
lazy abstraction
adopting a lazy strategy for cache refinement. Together, this achieves significant performance increases: our tool (an implementation within the configurable program analysis framework
CPAchecker
) has won the Competition on Software Verification 2012 in the category “Overall”.