Sciweavers

STTT
2016

Monitoring modulo theories

8 years 6 months ago
Monitoring modulo theories
This paper considers a generic approach to runtime verification of temporal properties over firstorder 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 (LTL) based on the Z3 SMT solver and evaluated regarding runtime performance.
Normann Decker, Martin Leucker, Daniel Thoma
Added 10 Apr 2016
Updated 10 Apr 2016
Type Journal
Year 2016
Where STTT
Authors Normann Decker, Martin Leucker, Daniel Thoma
Comments (0)