P. Cousot, On the Design of Program Logics

Patrick Cousot.
The Essence of Event-B from an Abstract Interpretation Perspective.
In Rigorous Engineering of Trustworhy Systems — Essays Dedicated to Jean-Raymond Abrial, Egon Börger and Yamine Aït Ameur (Eds), LNCS 16750, Springer, 2026.

Paper (29 pages): PDF (515 KB)

Abstract: We explain the basic concepts of Event-B, that is the specification of machines and refinement, in light of abstract interpretation. After formally defining the trace semantics of systems handled by Event-B, we show that machines are specifications of abstractions of this semantics while refinement is an inverse abstract interpretation reducing the degree of nondeterminism of this trace semantics. We conclude by proposing in induction principle for program verification exploiting both property abstraction and program refinement.
Keywords: Jean-Raymond Abrial Event-B · Abstraction · Abstract machine · Semantics · Refinement · Verification · Abstract interpretation · Formal methods.

\bibitem{AbrialGedenkschrift26}
Patrick Cousot.
\newblock The Essence of Event-B from an Abstract Interpretation Perspective.
\newblock In \emph{Rigorous Engineering of Trustworhy Systems -- 
   Essays Dedicated to Jean-Raymond Abrial},
   Egon Börger and Yamine Aït Ameur (Eds),
   29 pages, Springer, 2026

@inproceedings{AbrialGedenkschrift26,
   author =    {Patrick Cousot},
   title =     {The Essence of Event-B from an Abstract Interpretation Perspective},
   pages =     {29},
   booktitle = {Rigorous Engineering of Trustworhy Systems -- 
                Essays Dedicated to Jean-Raymond Abrial},
   editor    = {Egon Börger and Yamine Aït Ameur},
   publisher = {Springer},
   year =      2026,
 }

copyright notice
Last modified: Sun Sep 27 18:22:53 EDT 2026