{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:26:47Z","timestamp":1770751607731,"version":"3.50.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"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-11176-0_1","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:35Z","timestamp":1763842295000},"page":"3-26","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fuzz Testing with\u00a0Temporal Constraints"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tracy","family":"Clark","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vivek","family":"Reddy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Leucker, M., Reger, G.: An introduction to runtime verification. In: Lectures on Runtime Verification - Introductory and Advanced Topics. LNCS, vol. 10457, pp. 1\u201323. Springer (2018)","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-642-20398-5_3","volume-title":"NASA Formal Methods","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M.: The theory and practice of SALT. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 13\u201340. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_3"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Bersani, M. M., Rossi, M., San Pietro, P.: An SMT-based approach to satisfiability checking of MITL. Inf. Comput. 245, 72\u201397 (2015). https:\/\/doi.org\/10.1016\/J.IC.2015.06.007","DOI":"10.1016\/J.IC.2015.06.007"},{"key":"1_CR4","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 209\u2013224. USENIX (2008)"},{"issue":"4","key":"1_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1082983.1083249","volume":"30","author":"M d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. ACM SIGSOFT Softw. Eng. Not. 30(4), 1\u20137 (2005)","journal-title":"ACM SIGSOFT Softw. Eng. Not."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the Freeze Quantifier and Register Automata. Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 17\u201326. IEEE (2006)","DOI":"10.1109\/LICS.2006.31"},{"key":"1_CR7","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D., Kalus, G. (eds.) Engineering Dependable Software Systems. NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a034, pp. 141\u2013175. IOS Press (2013)"},{"key":"1_CR8","unstructured":"The Fuzz test case generator. https:\/\/github.com\/havelund\/fuzzing"},{"key":"1_CR9","unstructured":"Gerevini, A., Long, D.: Plan constraints and preferences in PDDL3, the language of the deterministic part of the fifth international planning competition. In: Fifth International Planning Competition, ICAPS (2006)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-540-69149-5_40","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K Havelund","year":"2008","unstructured":"Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 374\u2013383. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69149-5_40"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-75632-5_3","volume-title":"Lectures on Runtime Verification","author":"K Havelund","year":"2018","unstructured":"Havelund, K., Reger, G., Thoma, D., Z\u0103linescu, E.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 61\u2013102. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985). https:\/\/doi.org\/10.1145\/2455.2460","DOI":"10.1145\/2455.2460"},{"key":"1_CR14","unstructured":"Lark - a parsing toolkit for Python. https:\/\/github.com\/lark-parser\/lark"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Algebraic Program. 78(5), 293\u2013303 (2008). https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability checking for mission-time LTL. In: Computer Aided Verification, vol. 11562, pp. 3\u201322. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_1","DOI":"10.1007\/978-3-030-25543-5_1"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Milner, R.: A modal characterisation of observable machine-behaviour. In: CAAP 1981: Colloquium on Trees in Algebra and Programming, vol. 112, pp. 25\u201334. Springer (1981)","DOI":"10.1007\/3-540-10828-9_52"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"NASA Formal Methods","author":"J Peleska","year":"2011","unstructured":"Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 298\u2013312. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_22"},{"key":"1_CR19","unstructured":"Planning.Wiki. https:\/\/planning.wiki"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. 12, 123\u2013137 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0140-3","DOI":"10.1007\/s10009-010-0140-3"},{"key":"1_CR22","unstructured":"Scala Programming Language. http:\/\/www.scala-lang.org"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Proceedings of the 10th European Software Engineering Conference (ESEC\/FSE), pp. 263\u2013272. ACM (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"1_CR24","unstructured":"SMT-LIB. https:\/\/smt-lib.org"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: Proceedings of the 5th International Workshop on Runtime Verification (RV 2005), vol. 144(4), pp. 109\u2013124. Elsevier (2006)","DOI":"10.1016\/j.entcs.2006.02.007"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: Proceedings of the 2004 International Conference on Information Reuse and Integration, pp. 493\u2013498. IEEE (2004). https:\/\/doi.org\/10.1109\/IRI.2004.1431509","DOI":"10.1109\/IRI.2004.1431509"},{"key":"1_CR27","unstructured":"Triantafillou, E., Baier, J., McIlraith, S.: A unifying framework for planning with LTL and regular expressions. In: Proceedings of the Workshop on Model-Checking and Automated Planning (MOCHAP) at ICAPS, pp. 23\u201331 (2015)"},{"key":"1_CR28","unstructured":"Unified planning library. https:\/\/unified-planning.readthedocs.io\/en\/latest"},{"key":"1_CR29","unstructured":"The Z3 SMT solver. https:\/\/github.com\/z3prover\/z3"},{"key":"1_CR30","unstructured":"Zeller, A., Gopinath, R., B\u00f6hme, M., Fraser, G., Holler, C.: The Fuzzing Book. https:\/\/www.fuzzingbook.org"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:40Z","timestamp":1770721780000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","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":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}