Home | english  | Impressum | Sitemap | KIT

Predicate Abstraction in a Program Logic Calculus

Predicate Abstraction in a Program Logic Calculus
Autor(en):

Benjamin Weiß

Links:
Quelle:

7th International Conference on integrated Formal Methods (iFM 2009), Düsseldorf, Germany. LNCS 5423, Springer, 2009

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, where it allows 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

@inproceedings{Weiss2009,
  author       = {Benjamin Wei{\ss}},
  title        = {Predicate Abstraction in a Program Logic Calculus},
  editor       = {Michael Leuschel and Heike Wehrheim},
  booktitle    = {Proceedings, 7th International Conference on integrated Formal Methods (iFM 2009)},
  volume       = {5423},
  series       = {LNCS},
  pages        = {136--150},
  publisher    = {Springer},
  year         = {2009}
}