Monitoring modulo theories
| Title | Monitoring modulo theories |
| Publication Type | Journal Article |
| Year of Publication | 2016 |
| Authors | Decker, N, Leucker, M, Thoma, D |
| Journal | International Journal on Software Tools for Technology Transfer |
| Volume | 18 |
| Issue | 2 |
| Start Page | 205 |
| Pagination | 205-225 |
| ISSN | 1433-2779 |
| Keywords | First-order temporal logic, Monitor synthesis, Monitoring, Runtime verification, SMT |
| 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. |
| URL | http://dx.doi.org/10.1007/s10009-015-0380-3 |
| DOI | 10.1007/s10009-015-0380-3 |
| Refereed Designation | Refereed |
Bibtex:
@article {1173,
title = {Monitoring modulo theories},
journal = {International Journal on Software Tools for Technology Transfer},
volume = {18},
year = {2016},
pages = {205-225},
chapter = {205},
abstract = {<p>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.</p>
},
keywords = {First-order temporal logic, Monitor synthesis, Monitoring, Runtime verification, SMT},
issn = {1433-2779},
doi = {10.1007/s10009-015-0380-3},
url = {http://dx.doi.org/10.1007/s10009-015-0380-3},
author = {Normann Decker and Martin Leucker and Daniel Thoma}
}