Standard
Verified First-Order Monitoring with Recursive Rules. / Zingg, Sheila; Krstić, Srđan; Raszyk, Martin; Schneider, Joshua; Traytel, Dmitriy.
Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. ed. / Dana Fisman; Grigore Rosu. Vol. 2 Springer, 2022. p. 236-253 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13244 LNCS).
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
Zingg, S, Krstić, S, Raszyk, M, Schneider, J
& Traytel, D 2022,
Verified First-Order Monitoring with Recursive Rules. in D Fisman & G Rosu (eds),
Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. vol. 2, Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13244 LNCS, pp. 236-253, 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany,
02/04/2022.
https://doi.org/10.1007/978-3-030-99527-0_13APA
Zingg, S., Krstić, S., Raszyk, M., Schneider, J.
, & Traytel, D. (2022).
Verified First-Order Monitoring with Recursive Rules. In D. Fisman, & G. Rosu (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings (Vol. 2, pp. 236-253). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 13244 LNCS
https://doi.org/10.1007/978-3-030-99527-0_13Vancouver
Zingg S, Krstić S, Raszyk M, Schneider J
, Traytel D.
Verified First-Order Monitoring with Recursive Rules. In Fisman D, Rosu G, editors, Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. Vol. 2. Springer. 2022. p. 236-253. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13244 LNCS).
https://doi.org/10.1007/978-3-030-99527-0_13Author
Zingg, Sheila ; Krstić, Srđan ; Raszyk, Martin ; Schneider, Joshua ; Traytel, Dmitriy. / Verified First-Order Monitoring with Recursive Rules. Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings. editor / Dana Fisman ; Grigore Rosu. Vol. 2 Springer, 2022. pp. 236-253 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13244 LNCS).
Bibtex
@inproceedings{1bfb10d637dc4e5da5fa0adc3cf04092,
title = "Verified First-Order Monitoring with Recursive Rules",
abstract = "First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let{\textquoteright}s usefulness on several example specifications and evaluate our verified algorithm{\textquoteright}s performance against the DejaVu monitoring tool.",
keywords = "Formal verification, Monitoring, Rule-based specifications",
author = "Sheila Zingg and Sr{\d}an Krsti{\'c} and Martin Raszyk and Joshua Schneider and Dmitriy Traytel",
note = "Publisher Copyright: {\textcopyright} 2022, The Author(s).; 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022 ; Conference date: 02-04-2022 Through 07-04-2022",
year = "2022",
doi = "10.1007/978-3-030-99527-0_13",
language = "English",
isbn = "9783030995263",
volume = "2",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "236--253",
editor = "Dana Fisman and Grigore Rosu",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Switzerland",
}
RIS
TY - GEN
T1 - Verified First-Order Monitoring with Recursive Rules
AU - Zingg, Sheila
AU - Krstić, Srđan
AU - Raszyk, Martin
AU - Schneider, Joshua
AU - Traytel, Dmitriy
N1 - Publisher Copyright:
© 2022, The Author(s).
PY - 2022
Y1 - 2022
N2 - First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let’s usefulness on several example specifications and evaluate our verified algorithm’s performance against the DejaVu monitoring tool.
AB - First-order temporal logics and rule-based formalisms are two popular families of specification languages for monitoring. Each family has its advantages and only few monitoring tools support their combination. We extend metric first-order temporal logic (MFOTL) with a recursive let construct, which enables interleaving rules with temporal logic formulas. We also extend VeriMon, an MFOTL monitor whose correctness has been formally verified using the Isabelle proof assistant, to support the new construct. The extended correctness proof covers the interaction of the new construct with the existing verified algorithm, which is subtle due to the presence of the bounded future temporal operators. We demonstrate the recursive let’s usefulness on several example specifications and evaluate our verified algorithm’s performance against the DejaVu monitoring tool.
KW - Formal verification
KW - Monitoring
KW - Rule-based specifications
U2 - 10.1007/978-3-030-99527-0_13
DO - 10.1007/978-3-030-99527-0_13
M3 - Article in proceedings
AN - SCOPUS:85128729540
SN - 9783030995263
VL - 2
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 236
EP - 253
BT - Tools and Algorithms for the Construction and Analysis of Systems
A2 - Fisman, Dana
A2 - Rosu, Grigore
PB - Springer
T2 - 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 held as part of 25th European Joint Conferences on Theory and Practice of Software, ETAPS 2022
Y2 - 2 April 2022 through 7 April 2022
ER -
