Monitoring Modulo Theories
Title | Monitoring Modulo Theories |
Publication Type | Conference Paper |
Year of Publication | 2014 |
Authors | Decker, N, Leucker, M, Thoma, D |
Conference Name | Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014 |
Volume | LNCS 8413 |
Publisher | Springer |
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. |
DOI | 10.1007/978-3-642-54862-8_23 |
Bibtex:
@inproceedings {1013, title = {Monitoring Modulo Theories}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014}, volume = {LNCS 8413}, year = {2014}, publisher = {Springer}, organization = {Springer}, abstract = {<p>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.</p> }, doi = {http://dx.doi.org/10.1007/978-3-642-54862-8_23}, author = {Normann Decker and Martin Leucker and Daniel Thoma} }