Home | deutsch  | Legals | Sitemap | KIT

Predicate Abstraction in a Program Logic Calculus

Predicate Abstraction in a Program Logic Calculus
Author(s):

Benjamin Weiß

Links:
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.

BibTeX

@article{Weiss2011,
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},
}