Patrick Cousot, Non-Standard Hoare Logic

Patrick Cousot.
Non-Standard Hoare Logic
Formale Methoden in der Informatik, July 16-17, 2026, Leibniz Supercomputing Centre, Garching Forschungszentrum, Germany.
Slides of the 45mn presentation at Helmut Seidel's Fest:
- US letter, 55.4Mb,
Abstract:
The same way that Peano's naturals have non-standard models, there are non-standard trace semantics, with classic finite traces and forward infinite traces that start but never terminate as well as non-standard traces that never start but terminate or never start and never terminate, even in the transfinite. The abstraction of these semantics in Hoare triples yields the same Hoare logic, so that axiomatic semantics does not specify a unique semantics, up to an isomorphism. To do so, it is sufficient to prevent transfinite forward traces by adding Knuth termination requirement at ω (omega) for forward traces and it's inverse for infinite backward traces. This is an additional requirement in axiomatic semantics but not in Hoare logic since everybody implicitly applies it to standard trace semantics.
Keywords:
Formal methods, Non-Standard Trace Semantics, Hoare Logiv, Axiomatic Semantics, Abstraction, Abstract interpretation.

Bibliographic reference:

@inproceedings{Cousot-HelmutSeidelFest2026,
  author    = {Patrick Cousot},
  title     = {Non-Standard Hoare Logic},
  booktitle = {Formale Methoden in der Informatik, Leibniz Supercomputing 
               Centre, Garching Forschungszentrum, Germany},
  month     = jul,
  year      = {2026},
  url       = {https://helmutfest.github.io/},
}

\bibitem{Cousot-HelmutSeidelFest2026}
Patrick Cousot.
\newblock Non-Standard Hoare Logic.
\newblock In \emph{Formale Methoden in der Informatik}, July 16-17, 2026, 
          Leibniz Supercomputing Centre, Garching Forschungszentrum, Germany.
          (\url{{https://helmutfest.github.io/}}).

copyright notice
Last modified: Thu Jul 16 12:12:33 CEST 2026