• Patrick Cousot.
    Nonstandard Axiomatic Semantics.
     In Proc. ICTAC 2026, November 9--15, 2026, Bariloche, Argentina, Springer, 16 pages.

  • Paper (16 pages): PDF (160 KB)

  • Abstract: Similar to Skolem's nonstandard models of Peano's naturals, we show that axiomatic semantics based on Hoare logic has nonstandard models and so does not specify a unique, well-defined, and formal operational semantics of programming languages. We propose to enrich axiomatic semantics with additional proof obligations to solve this ambiguity problem. These proof obligations are always satisfied for standard trace models so that Hoare logic proofs are unchanged for these standard models.

  • https://doi.org/10.48550/arXiv.2608.22998

  • Slides (TBA) PDF format (47.2 MB). 

  • \bibitem{Cousot-ICTAC2026-1}
Patrick Cousot.
\newblock Calculational Design of Hyperlogics by Abstract Interpretation.
\newblock In \emph{Proc. ICTAC 2026}, Bariloche, Argentina, Springer, 2026
  

@inproceedings{Cousot-ICTAC2026-1,
   author =    {Patrick Cousot},
   title =     {Nonstandard Axiomatic Semantics},
   booktitle = {Proc. ICTAC 2026},
   address =   {Bariloche, Argentina},
   publisher = {Springer},
   year =      2026,
}

    copyright notice
    Last modified: Tuesday, 25-Aug-2026 03:46:15 EDT