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

Institut für Softwaretechnik und Programmiersprachen

28 Zitate (Scopus)

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.

Originalsprache	Englisch
Titel	Tools and Algorithms for the Construction and Analysis of Systems
Seitenumfang	16
Band	8413
Erscheinungsort	Berlin
Herausgeber (Verlag)	Springer Verlag
Erscheinungsdatum	01.04.2014
Seiten	341-356
ISBN (Print)	978-3-642-54861-1
ISBN (elektronisch)	978-3-642-54862-8
DOIs	https://doi.org/10.1007/978-3-642-54862-8_23
Publikationsstatus	Veröffentlicht - 01.04.2014
Veranstaltung	20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Grenoble, Frankreich Dauer: 05.04.2014 → 13.04.2014 Konferenznummer: 105112

UN SDGs

Dieser Output leistet einen Beitrag zu folgendem(n) Ziel(en) für nachhaltige Entwicklung

SDG 9 – Industrie, Innovation und Infrastruktur

Zugriff auf Dokument

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

Andere Dateien und Links

https://www.scopus.com/pages/publications/84900543237

Dieses zitieren

@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 . Bd. 8413, Lecture Notes in Computer Science, Bd. 8413, Springer Verlag, Berlin, S. 341-356, 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Grenoble, Frankreich, 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/pages/publications/84900543237

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

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Dieses zitieren