- Conference Paper
Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness proof in Isabelle/HOL of a monitor for metric first-order dynamic logic. This monitor significantly extends previous work on formally verified monitors by supporting aggregations, regular expressions (the dynamic part), and optimizations including multi-way joins adopted from databases and a new sliding window algorithm. Show more
Book titleAutomated Reasoning
Journal / seriesLecture Notes in Computer Science
Pages / Article No.
Organisational unit03634 - Basin, David / Basin, David
167162 - Big Data Monitoring (SNF)
NotesDue to the Coronavirus (COVID-19) the conference was conducted virtually.
MoreShow all metadata