About: A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Creator	Basin, David Dardinier, Thibault Heimes, Lukas Krstić, Srđan Raszyk, Martin Schneider, Joshua Traytel, Dmitriy
Source	PMC
abstract	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.
has issue date	2020-05-30(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51074-9_25
has license	no-cc
sha1sum (hex)	69076fe802fab77b5a9137e0493a1526be9b2989
schema:url	https://doi.org/10.1007/978-3-030-51074-9_25
resource representing a document's title	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
has PubMed Central identifier	PMC7324294
schema:publication	Automated Reasoning
resource representing a document's body	covid:69076fe802fab77b5a9137e0493a1526be9b2989#body_text
is schema:about of	named entity 'INCLUDING' named entity 'DYNAMIC' named entity 'regular expressions' named entity 'formally verified' named entity 'Formally Verified' named entity 'automaton' named entity 'Isabelle' named entity 'time-stamps' named entity 'recursion' named entity 'syntax' named entity 'conjunctions' named entity 'first-order' named entity 'conjunctions' named entity 'time-point' named entity 'master's thesis' named entity 'regular expressions' named entity 'Isabelle' named entity 'ith' named entity 'disjoint' named entity 'free variables' named entity 'time-point' named entity 'regular expressions' named entity 'regular expression' named entity 'data values' named entity 'differential testing' named entity 'tuple' named entity 'sequences of events' named entity 'syntactic' named entity 'multi-way' named entity 'semantics' named entity 'time-stamp' named entity 'multi-way' named entity 'disjunction' named entity 'multi-way' named entity 'timestamp' named entity 'specification language' named entity 'binary relation' named entity 'time-point' named entity 'regular expressions' named entity 'regular expressions' named entity 'data values' named entity 'algorithm' named entity 'Time-stamps' named entity 'free variables' named entity 'dynamic logic' named entity 'garbage collection' named entity 'lexicographically' named entity 'first-order' named entity 'SQL' named entity 'conjunctions' named entity 'time-point' named entity 'user interface' named entity 'natural numbers' named entity 'Kleene star' named entity 'time-stamp' named entity 'recursively' named entity 'optimization' named entity 'recursion' named entity 'datatype' named entity 'multi-way' named entity 'multi-way' named entity 'time-stamp' named entity 'strictly increasing' named entity 'subformula' named entity 'syntax' named entity 'free variables' named entity 'aggregation functions' named entity 'predicate' named entity 'regular expressions' named entity 'algorithm' named entity 'differential testing' named entity 'iff' named entity 'relation composition' named entity 'first-order' named entity 'tuple' named entity 'Isabelle' named entity 'ith'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software