A formally verified, optimized monitor for metric first-order dynamic logic
From MaRDI portal
Publication:2096466
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
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
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
