Efficient Runtime Verification of First-Order Temporal Properties

DOI10.1007/978-3-319-94111-0_2MaRDI QIDQ5883570zbMATH OpenOpenAlexFDO

Authors Klaus Havelund, Doron Peled

Publication date 21 March 2023

Published in Model Checking Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-94111-0_2

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• First-order temporal logic monitoring with BDDs
• First-Order Timed Runtime Verification Using BDDs
• Monitoring metric first-order temporal properties
• Runtime monitoring of metric first-order temporal properties
• Monitoring first-order interval logic

Cites work

• Completing the temporal picture
• scientific article; zbMATH DE number 2080059 (Why is no real title available?)
• Monitoring metric first-order temporal properties
• Programming Languages and Systems
• Proving the Correctness of Multiprocess Programs
• Recognizing safety and liveness
• Verification, Model Checking, and Abstract Interpretation

Cited in

(15)

• Declarative stream runtime verification (hLola)
• A formally verified, optimized monitor for metric first-order dynamic logic
• Runtime verification of temporal properties over out-of-order data streams
• First-order temporal logic monitoring with BDDs
• Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
• Monitoring metric first-order temporal properties
• Runtime monitoring of metric first-order temporal properties
• Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation
• Quantified event automata: towards expressive and efficient runtime monitors
• Runtime verification based on register automata
• Monitoring first-order interval logic
• Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic
• First-Order Timed Runtime Verification Using BDDs
• Probabilistic Metric Temporal Graph Logic
• The ins and outs of first-order runtime verification

Describes a project that uses

Uses Software

• MONA
• Java-MOP
• LARVA
• GitHub

This page was built for publication: Efficient Runtime Verification of First-Order Temporal Properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5883570)