Monitoring modulo theories

Normann Decker*, Martin Leucker, Daniel Thoma

*Korrespondierende/r Autor/-in für diese Arbeit
10 Zitate (Scopus)

Abstract

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.

OriginalspracheEnglisch
ZeitschriftInternational Journal on Software Tools for Technology Transfer
Jahrgang18
Ausgabenummer2
Seiten (von - bis)205-225
Seitenumfang21
ISSN1433-2779
DOIs
PublikationsstatusVeröffentlicht - 01.04.2016

Fingerprint

Untersuchen Sie die Forschungsthemen von „Monitoring modulo theories“. Zusammen bilden sie einen einzigartigen Fingerprint.

Zitieren