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}
}