{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:45:59Z","timestamp":1766043959500,"version":"3.48.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032054340"},{"type":"electronic","value":"9783032054357"}],"license":[{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,9,12]],"date-time":"2025-09-12T00:00:00Z","timestamp":1757635200000},"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-032-05435-7_2","type":"book-chapter","created":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T01:30:33Z","timestamp":1757727033000},"page":"22-43","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["DSLs for\u00a0Runtime Verification"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Moran","family":"Omer","sequence":"additional","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,9,12]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Aichernig, B., Havelund, K.: Correct-ish by design: from upfront verification to continuous monitoring of LLM generated code. In: Steffen, B. (ed.) AISoLA 2024: Bridging the Gap Between AI and Reality. Springer, Heidelberg (2025)","DOI":"10.1007\/978-3-032-01377-4_1"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"Model Checking Software","author":"A Armando","year":"2006","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 146\u2013162. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691617_9"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-21437-0_7","volume-title":"FM 2011: Formal Methods","author":"H Barringer","year":"2011","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"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-77395-5_10","volume-title":"Runtime Verification","author":"H Barringer","year":"2007","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"},{"key":"2_CR5","doi-asserted-by":"publisher","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","DOI":"10.1007\/s10703-015-0222-7"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Cohen, I., Havelund, K., Peled, D., Goldberg, Y.: The power of reframing: using LLMs in synthesizing RV monitors. In: K\u00f6nighofer, B., Torfah, H. (eds.) 25th International Conference on Runtime Verification (RV). LNCS. Springer, Heidelberg (2025)","DOI":"10.1007\/978-3-032-05435-7_12"},{"key":"2_CR7","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":"2_CR8","doi-asserted-by":"publisher","unstructured":"Dams, D., Havelund, K., Kauffman, S.: A Python library for trace analysis. In: Dang, T., Stolz, V. (eds.) 22nd International Conference on Runtime Verification (RV), vol. 13498 of LNCS, pp. 264\u2013273. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_15","DOI":"10.1007\/978-3-031-17196-3_15"},{"key":"2_CR9","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\u201905), pp. 166\u2013174(2005)","DOI":"10.1109\/TIME.2005.26"},{"issue":"2","key":"2_CR10","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":"2_CR11","unstructured":"DejaVu tool source code. https:\/\/github.com\/havelund\/dejavu"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Duckett, B., Havelund, K., Stewart, L.: Space telemetry analysis with PyContract. In: Haxthausen, A.E., Huang, W., Roggenbach, M. (eds.) Applicable Formal Methods for Safe Industrial Products - Essays Dedicated to Jan Peleska on the Occasion of His 65th Birthday, vol. 14165 of LNCS. Springer, Heidelberg (2023)","DOI":"10.1007\/978-3-031-40132-9_17"},{"key":"2_CR13","unstructured":"Andy Dustman. Python MySQL (2024). https:\/\/pypi.org\/project\/MySQL-python\/"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169\u2013181. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10003-2_69","DOI":"10.1007\/3-540-10003-2_69"},{"key":"2_CR15","unstructured":"Gemini large language model. https:\/\/gemini.google.com"},{"key":"2_CR16","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":"2_CR17","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Halle","year":"2012","unstructured":"Halle, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5, 192\u2013206 (2012)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"2_CR18","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":"2_CR19","first-page":"143","volume":"17","author":"K Havelund","year":"2015","unstructured":"Havelund, K.: Rule-based runtime verification revisited. Softw. Tools Technol. Transf. (STTT) 17(2), 143\u2013170 (2015)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"2_CR20","unstructured":"Havelund, K.: Daut - Monitoring Data Streams with Data Automata (2024). https:\/\/github.com\/havelund\/daut"},{"key":"2_CR21","doi-asserted-by":"publisher","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.) Verification, Model Checking, and Abstract Interpretation, pp. 249\u2013263. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-50521-8_12","DOI":"10.1007\/978-3-031-50521-8_12"},{"key":"2_CR22","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"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Havelund, K., Peled, D.: An extension of first-order LTL with rules with application to runtime verification. Int. J. Softw. Tools Technol. Transf. 23(4), 547\u2013563 (2021). https:\/\/doi.org\/10.1007\/s10009-021-00626-y","DOI":"10.1007\/s10009-021-00626-y"},{"issue":"1\u20133","key":"2_CR24","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":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"2_CR26","unstructured":"Top programming languages (2024). https:\/\/spectrum.ieee.org\/top-programming-languages-2024"},{"key":"2_CR27","unstructured":"Johnson, S.C.: Yacc: yet another compiler-compiler. https:\/\/en.wikipedia.org\/wiki\/Yacc"},{"key":"2_CR28","doi-asserted-by":"publisher","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.) Runtime Verification, pp. 314\u2013324. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17196-3_20","DOI":"10.1007\/978-3-031-17196-3_20"},{"key":"2_CR29","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":"2_CR30","unstructured":"Matiyasevich, Y.: Hilbert\u2019s 10th Problem. MIT Press, Cambridge (1993)"},{"key":"2_CR31","first-page":"249","volume":"14","author":"PON Meredith","year":"2011","unstructured":"Meredith, P.O.N., Jin, D., Griffith, D., Chen, F., Ro\u015fu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Techn. Technol. Transf. 14, 249\u2013289 (2011)","journal-title":"Int. J. Softw. Techn. Technol. Transf."},{"key":"2_CR32","unstructured":"PyContract. https:\/\/github.com\/pyrv\/pycontract"},{"key":"2_CR33","unstructured":"PyDejaVu tool source code. https:\/\/github.com\/moraneus\/pydejavu"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Queille, J.P., Sifakis, J.: Iterative methods for the analysis of petri nets. In: Girault, C., Reisig, W. (eds.) Application and Theory of Petri Nets, Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, Strasbourg, France, 23\u201326 September 1980, Bad Honnef, Germany, 28\u201330 September 1981, vol.\u00a052 of Informatik-Fachberichte, pp. 161\u2013167. Springer, Heidelberg (1981). https:\/\/doi.org\/10.1007\/978-3-642-68353-4_27","DOI":"10.1007\/978-3-642-68353-4_27"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/978-3-662-46681-0_55","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2015","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"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133\u2013191. Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"2_CR37","unstructured":"TP-DejaVu tool source code. https:\/\/github.com\/moraneus\/TP-DejaVu"},{"key":"2_CR38","unstructured":"Windsurf editor. https:\/\/windsurf.com"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-05435-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T07:43:09Z","timestamp":1766043789000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-05435-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,12]]},"ISBN":["9783032054340","9783032054357"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-05435-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,9,12]]},"assertion":[{"value":"12 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Runtime Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Graz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rv2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rv25.isec.tugraz.at\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}