Logic and Formal Methods

Predicate Abstraction in a Program Logic Calculus

  • Author(s):

    Benjamin Weiß

  • Source:

    Science of Computer Programming 76 (10), Elsevier, 2011

  • Predicate abstraction is a form of abstract interpretation where the abstract domain is constructed from a finite set of predicates over the variables of the program. This paper explores a way to integrate predicate abstraction into a calculus for deductive program verification based on symbolic execution, where it allows us to infer loop invariants automatically that would otherwise have to be given interactively. The approach has been implemented as a part of the KeY verification system.


author = {Benjamin Wei{\ss}},
title = {Predicate Abstraction in a Program Logic Calculus},
journal = {Science of Computer Programming},
volume = {76},
number = {10},
pages = {861--876},
year = {2011},