Monitoring modulo theories

Normann Decker; Martin Leucker; Daniel Thoma

doi:10.1007/s10009-015-0380-3

Monitoring modulo theories

Normann Decker^*, Martin Leucker, Daniel Thoma

^*Corresponding author for this work

Institute of Software Engineering and Programming Languages

40 Citations (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.

Original language	English
Journal	International Journal on Software Tools for Technology Transfer
Volume	18
Issue number	2
Pages (from-to)	205-225
Number of pages	21
ISSN	1433-2779
DOIs	https://doi.org/10.1007/s10009-015-0380-3
Publication status	Published - 01.04.2016

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/s10009-015-0380-3

Cite this

@article{2f416e53be1e4a5e810adcbaac73d41f,

title = "Monitoring modulo theories",

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.",

author = "Normann Decker and Martin Leucker and Daniel Thoma",

year = "2016",

month = apr,

day = "1",

doi = "10.1007/s10009-015-0380-3",

language = "English",

volume = "18",

pages = "205--225",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2779",

publisher = "Springer Verlag",

number = "2",

}

TY - JOUR

T1 - Monitoring modulo theories

AU - Decker, Normann

AU - Leucker, Martin

AU - Thoma, Daniel

PY - 2016/4/1

Y1 - 2016/4/1

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84961050189

U2 - 10.1007/s10009-015-0380-3

DO - 10.1007/s10009-015-0380-3

M3 - Journal articles

AN - SCOPUS:84961050189

SN - 1433-2779

VL - 18

SP - 205

EP - 225

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 2

ER -

Monitoring modulo theories

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this