Temporal logics are widely used in runtime verification as they enable the creation of
declarative and compositional specifications. However, their ability to model complex data is …

Modern software systems must comply with increasingly complex regulations in domains
ranging from industrial automation to data protection. Runtime enforcement addresses this …

Runtime enforcement is a dynamic analysis technique that instruments a monitor with a
system in order to ensure its correctness as specified by some property. This paper explores …

The MonPoly project started over a decade ago to build effective tools for monitoring trace
properties, including functional correctness, security, and compliance policies. The original …

First-order monitors analyze data-carrying event streams. When event streams are
generated by distributed systems, it may be difficult to ensure that events arrive at the …

We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations),
a framework for the verification of cyber-physical systems. We describe the semantic …

Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a
specification logic, eg, for runtime verification, model checking, and other formal methods …

Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification
logics like STL and MTL, is often used to model and verify real world systems in safety …

Runtime verification describes techniques in which individual runs of a system, typically
represented as traces, are inspected for desired or undesired properties. The central …

First-order monitors analyze data-carrying event streams. When event streams are
generated by distributed systems, it may be difficult to ensure that events arrive at the …