A formally verified, optimized monitor for metric first-order dynamic logic

DOI10.1007/978-3-030-51074-9_25OpenAlexW3039218154MaRDI QIDQ2096466

Dmitriy Traytel, Martin Raszyk, Joshua Schneider, Srđan Krstić, Thibault Dardinier, Lukas Heimes, David A. Basin

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_25

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Real-time policy enforcement with metric first-order temporal logic ⋮ VeriMon: a formally verified monitoring tool ⋮ A theory of monitors

Uses Software

• ModelPlex
• Archive Formal Proofs
• aerial
• MonPoly

Cites Work

• Unnamed Item
• Unnamed Item
• Greedily computing associative aggregations on sliding windows
• Partial derivatives of regular expressions and finite automaton constructions
• ModelPlex: verified runtime validation of verified cyber-physical system models
• Monitoring of temporal first-order properties with aggregations
• The ins and outs of first-order runtime verification
• Refinement to imperative HOL
• A Coq formalisation of SQL's execution engines
• Almost event-rate independent monitoring
• Monitoring Metric First-Order Temporal Properties
• Regular Programming for Quantitative Properties of Data Streams
• Multi-head Monitoring of Metric Temporal Logic
• Worst-case Optimal Join Algorithms
• Communication Steps for Parallel Query Processing
• Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors
• Toward a verified relational database management system
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
• Derivatives of Regular Expressions
• Efficient Runtime Verification of First-Order Temporal Properties

This page was built for publication: A formally verified, optimized monitor for metric first-order dynamic logic