Monitoring Modulo Theories

Normann Decker; Martin Leucker; Daniel Thoma

doi:10.1007/978-3-642-54862-8_23

Monitoring Modulo Theories

Normann Decker, Martin Leucker, Daniel Thoma

Institute of Software Engineering and Programming Languages

Abstract

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 language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Number of pages	16
Volume	8413
Place of Publication	Berlin
Publisher	Springer Verlag
Publication date	01.04.2014
Pages	341-356
ISBN (Print)	978-3-642-54861-1
ISBN (Electronic)	978-3-642-54862-8
DOIs	https://doi.org/10.1007/978-3-642-54862-8_23
Publication status	Published - 01.04.2014
Event	20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Grenoble, France Duration: 05.04.2014 → 13.04.2014 Conference number: 105112

UN SDGs

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

Access to Document

10.1007/978-3-642-54862-8_23

Cite this

@inproceedings{3967a398e08940238da3b564e357bca9,

title = "Monitoring Modulo Theories",

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

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

year = "2014",

month = apr,

day = "1",

doi = "10.1007/978-3-642-54862-8_23",

language = "English",

isbn = "978-3-642-54861-1",

volume = "8413",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "341--356",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

note = "20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , TACAS 2014 ; Conference date: 05-04-2014 Through 13-04-2014",

}

Decker, N, Leucker, M & Thoma, D 2014, Monitoring Modulo Theories. in Tools and Algorithms for the Construction and Analysis of Systems . vol. 8413, Lecture Notes in Computer Science, vol. 8413, Springer Verlag, Berlin, pp. 341-356, 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Grenoble, France, 05.04.14. https://doi.org/10.1007/978-3-642-54862-8_23

TY - GEN

T1 - Monitoring Modulo Theories

AU - Decker, Normann

AU - Leucker, Martin

AU - Thoma, Daniel

N1 - Conference code: 105112

PY - 2014/4/1

Y1 - 2014/4/1

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

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

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-84900543237&origin=inward&txGid=c8728b8c79ff7fc4f36d2a9ed6e0c11b

U2 - 10.1007/978-3-642-54862-8_23

DO - 10.1007/978-3-642-54862-8_23

M3 - Conference contribution

SN - 978-3-642-54861-1

VL - 8413

T3 - Lecture Notes in Computer Science

SP - 341

EP - 356

BT - Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer Verlag

CY - Berlin

T2 - 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Y2 - 5 April 2014 through 13 April 2014

ER -

Monitoring Modulo Theories

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this