P. Cousot, On the Design of Program Logics

Patrick Cousot.
On the Design of Program Logics.
In Andreas Podelski Festschrift, Springer, 2024
Paper (15 pages): PDF (153 KB)

Abstract: We illustrate the sound and complete construction of program logics by abstraction of a relational semantics into the theory of the logic followed by the formal derivation of the proof system. We consider Hoare logic, O’Hearn incorrectness logic and Hoare incorrectness logic formalizing debugging.
Keywords: Hoare logic · reverse Hoare logic · incorrectness logic · Hoare incorrectness logic · debugging · abstract interpretation.

\bibitem{PodelskiFestschrift24}
Patrick Cousot.
\newblock On the Design of Program Logics.
\newblock In \emph{Andreas Podelski Festschrift}
  15 pages, Springer

@inproceedings{PodelskiFestschrift24,
   author =    {Patrick Cousot},
   title =     {On the Design of Program Logics},
   pages =     {15},
   booktitle = {Andreas Podelski Festschrift},
   publisher = {Springer},
   year =      2024,
 }

copyright notice
Last modified: Saturday, 27-Jan-2024 11:08:22 EST