A formally verified, optimized monitor for metric first-order dynamic logic
From MaRDI portal
Publication:2096466
Cites work
- A Coq formalisation of SQL's execution engines
- Almost event-rate independent monitoring
- Communication steps for parallel query processing
- Derivatives of Regular Expressions
- Efficient Runtime Verification of First-Order Temporal Properties
- Greedily computing associative aggregations on sliding windows
- scientific article; zbMATH DE number 2080059 (Why is no real title available?)
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Light-weight containers for Isabelle: efficient, extensible, nestable
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Monitoring metric first-order temporal properties
- Monitoring of temporal first-order properties with aggregations
- Multi-head monitoring of metric temporal logic
- Partial derivatives of regular expressions and finite automaton constructions
- Quantified event automata: towards expressive and efficient runtime monitors
- Refinement to imperative HOL
- Regular Programming for Quantitative Properties of Data Streams
- The ins and outs of first-order runtime verification
- Toward a verified relational database management system
- Worst-case optimal join algorithms
Cited in
(7)- A theory of monitors
- Monitor Logics for Quantitative Monitor Automata
- Real-time policy enforcement with metric first-order temporal logic
- VeriMon: a formally verified monitoring tool
- Hammering Floating-Point Arithmetic
- Verified first-order monitoring with recursive rules
- Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
This page was built for publication: A formally verified, optimized monitor for metric first-order dynamic logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096466)
