Monitoring modulo theories

Normann Decker*, Martin Leucker, Daniel Thoma

*Corresponding author for this work
10 Citations (Scopus)


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

Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Issue number2
Pages (from-to)205-225
Number of pages21
Publication statusPublished - 01.04.2016


Dive into the research topics of 'Monitoring modulo theories'. Together they form a unique fingerprint.

Cite this