Patrick Cousot and Radhia Cousot.<bR> Abstract Hoare Logic.

Patrick Cousot and Radhia Cousot.
Abstract Hoare Logic.
In Pre-POPL Yak International, CIMS, NYU, January 21st, 2011.
Slides: 1/1 (PDF, 166 KB), 4/1 (PDF, 151 KB)
Abstract: Hoare logic uses predicates expressed in a first-order logic interpreted in set-theory. It has implicit conjunction and disjunction (which can be derived from the other rules). When, instead, the predicates belong to an abstract domain these rules may be unsound which has infortunate consequences for the method/procedure call rules. We provide sufficient soundness conditions.
Categories and Subject Descriptors: D.2.4 [Software/Program Verification];
D.3.1 [Formal Definitions and Theory];
F.3.1 [Specifying and Verifying and Reasoning about Programs].
General Terms: Languages, Reliability, Security, Theory, Verification.
Keywords: Abstract domain, Abstract Interpretation, Hoare Logic, Induction, Proof, Safety.

Bibliographic reference:

\bibitem{CousotCousot-2012-01-21-Pre-POPL-Yak}
P.~Cousot and R.~Cousot.
\newblock Abstract Hoare Logic.
\newblock In Pre-POPL Yak International, CIMS, NYU, January 21st,  2011.

@inproceedings{CousotCousot-2012-01-21-Pre-POPL-Yak,
  author    = {Patrick Cousot and
               Radhia Cousot},
  title     = {Abstract Hoare Logic},
  booktitle = {Pre-POPL Yak International, CIMS, NYU},
  month     = jan # " 21st",
  year      = {2011},
}

copyright notice
Last modified: Sun May 11 09:52:57 EDT 2014