{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T23:51:56Z","timestamp":1777765916204,"version":"3.51.4"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031974380","type":"print"},{"value":"9783031974397","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-97439-7_13","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:04:09Z","timestamp":1756551849000},"page":"266-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Embedding Monitoring of\u00a0First-Order Temporal Logic in\u00a0a\u00a0Programming Language"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moran","family":"Omer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Barringer, H., Havelund, K.: TraceContract: a scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57\u201372. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_7","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 111\u2013125. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77395-5_10","DOI":"10.1007\/978-3-540-77395-5_10"},{"issue":"3","key":"13_CR3","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-015-0222-7","volume":"46","author":"D Basin","year":"2015","unstructured":"Basin, D., Klaedtke, F., Marinovic, S., Z\u0103linescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262\u2013285 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0222-7","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-16612-9_38","volume-title":"Runtime Verification","author":"C Colombo","year":"2010","unstructured":"Colombo, C., Gauci, A., Pace, G.J.: LarvaStat: monitoring of statistical properties. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 480\u2013484. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_38"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Dams, D., Havelund, K., Kauffman, S.: A Python library for trace analysis. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 264\u2013273. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_15","DOI":"10.1007\/978-3-031-17196-3_15"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., et al.: Lola: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"issue":"2","key":"13_CR7","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10009-015-0380-3","volume":"18","author":"N Decker","year":"2016","unstructured":"Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18(2), 205\u2013225 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR8","unstructured":"DejaVu tool source code. https:\/\/github.com\/havelund\/dejavu"},{"key":"13_CR9","unstructured":"Andy Dustman. Python MySQL (2024). https:\/\/pypi.org\/project\/MySQL-python\/"},{"key":"13_CR10","unstructured":"Github. Pytorch (2024). https:\/\/github.com\/pytorch\/pytorch"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/978-3-030-90870-6_30","volume-title":"Formal Methods","author":"F Gorostiaga","year":"2021","unstructured":"Gorostiaga, F., S\u00e1nchez, C.: HStriver: a very functional extensible tool for the runtime verification of real-time event streams. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 563\u2013580. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_30"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Halle, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. 5, 192\u2013206 (2012)","DOI":"10.1109\/TSC.2011.10"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Havelund, K.: Data automata in Scala. In: 2014 Theoretical Aspects of Software Engineering Conference, TASE 2014, Changsha, China, 1\u20133 September 2014, pp. 1\u20139. IEEE Computer Society (2014)","DOI":"10.1109\/TASE.2014.37"},{"issue":"2","key":"13_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10009-014-0309-2","volume":"17","author":"K Havelund","year":"2015","unstructured":"Havelund, K.: Rule-based runtime verification revisited. Softw. Tools Technol. Transfer (STTT) 17(2), 143\u2013170 (2015)","journal-title":"Softw. Tools Technol. Transfer (STTT)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-031-50521-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K Havelund","year":"2024","unstructured":"Havelund, K., Katsaros, P., Omer, M., Peled, D., Temperekidis, A.: TP-DejaVu: combining operational and declarative runtime verification. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) VMCAI 2024. LNCS, vol. 14500, pp. 249\u2013263. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-50521-8_12"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Havelund, K., Omer, M., Peled, D.: Operational and declarative runtime verification (keynote). In: Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution, VORTEX 2024, pp. 3\u201312. Association for Computing Machinery, New York (2024)","DOI":"10.1145\/3679008.3685541"},{"issue":"4","key":"13_CR17","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/s10009-021-00626-y","volume":"23","author":"K Havelund","year":"2021","unstructured":"Havelund, K., Peled, D.: An extension of first-order LTL with rules with application to runtime verification. Int. J. Softw. Tools Technol. Transfer 23(4), 547\u2013563 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00626-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1\u20133","key":"13_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-018-00327-4","volume":"56","author":"K Havelund","year":"2020","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. Formal Methods Syst. Des. 56(1\u20133), 1\u201321 (2020)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR19","unstructured":"Haveund, K.: Daut - Monitoring Data Streams with Data Automata (2024). https:\/\/github.com\/havelund\/daut"},{"key":"13_CR20","unstructured":"Johnson, S.C.: YACC: Yet Another Compiler-Compiler. https:\/\/en.wikipedia.org\/wiki\/Yacc"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-031-17196-3_20","volume-title":"Runtime Verification","author":"H Kallwies","year":"2022","unstructured":"Kallwies, H., Leucker, M., Schmitz, M., Schulz, A., Thoma, D., Weiss, A.: TeSSLa \u2013 an ecosystem for runtime verification. In: Dang, T., Stolz, V. (eds.) RV 2022. LNCS, vol. 13498, pp. 314\u2013324. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_20"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/3-540-45337-7_18","volume-title":"ECOOP 2001 \u2014 Object-Oriented Programming","author":"G Kiczales","year":"2001","unstructured":"Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327\u2013354. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45337-7_18"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Java-MaC: a run-time assurance tool for Java programs. In: Havelund, K., Rosu, G. (eds.) Workshop on Runtime Verification, RV 2001, in connection with CAV 2001, Paris, France, 23 July 2001. Electronic Notes in Theoretical Computer Science, vol.\u00a055, pp. 218\u2013235. Elsevier (2001)","DOI":"10.1016\/S1571-0661(04)00254-3"},{"key":"13_CR24","unstructured":"PyDejaVu tool source code. https:\/\/github.com\/moraneus\/pydejavu"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 596\u2013610. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_55","DOI":"10.1007\/978-3-662-46681-0_55"},{"key":"13_CR26","unstructured":"TPDejaVu tool source code. https:\/\/doi.org\/10.5281\/zenodo.8322559"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T15:30:28Z","timestamp":1777476628000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}