Email Gateway (Apr 19 2024 at 11:34): Email Gateway (Apr 19 2024 at 11:34):From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce the following new AFP entry:
A Verified Proof Checker for Metric First-Order Temporal Logic
by
Andrei Herasimau, Jonathan Julian Huerta y Munive, Leonardo Lima,
Martin Raszyk and Dmitriy Traytel
Metric first-order temporal logic (MFOTL) is an expressive formalism for
specifying temporal and data-dependent constraints on streams of time-stamped,
data-carrying events. Recently, we have developed a monitoring algorithm that
not only outputs the satisfaction or violation of MFOTL formulas but also
explains its verdicts in the form of proof trees. These explanations serve as
certificates, and in this entry we verify the correctness of a certificate
checker. The checker is used to certify the output of our new, unverified
monitoring tool WhyMon. The formalization contains another unverified,
executable implementation of an explanation-producing monitoring algorithm used
to exemplify our checker.
https://www.isa-afp.org/entries/MFOTL_Checker.html
Enjoy,
René
Last updated: May 04 2024 at 20:16 UTC