This paper considers a generic approach to enhance traditional runtime verification techniques towards first-order theories in order to reason about data. This allows especially for the verification of multi-threaded, object-oriented systems. It presents a general framework lifting the monitor synthesis for propositional temporal logics to a temporal logic over structures within some first-order theory. To evaluate such temporal properties, SMT solving and classical monitoring of propositional temporal properties is combined. The monitoring procedure was implemented for linear-time temporal logic (LTL) based on the Z3 SMT solver and evaluated regarding runtime performance.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Number of pages16
Place of PublicationBerlin
PublisherSpringer Verlag
Publication date01.04.2014
ISBN (Print)978-3-642-54861-1
ISBN (Electronic)978-3-642-54862-8
Publication statusPublished - 01.04.2014
Event20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Grenoble, France
Duration: 05.04.201413.04.2014
Conference number: 105112


Dive into the research topics of 'Monitoring Modulo Theories'. Together they form a unique fingerprint.

Cite this