{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T02:42:26Z","timestamp":1772505746349,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2019,1,7]],"date-time":"2019-01-07T00:00:00Z","timestamp":1546819200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,1,7]],"date-time":"2019-01-07T00:00:00Z","timestamp":1546819200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100006196","name":"Jet Propulsion Laboratory","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006196","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Verimag"},{"DOI":"10.13039\/501100002744","name":"Bar-Ilan University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002744","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10703-018-00327-4","type":"journal-article","created":{"date-parts":[[2019,1,8]],"date-time":"2019-01-08T18:52:06Z","timestamp":1546973526000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["First-order temporal logic monitoring with BDDs"],"prefix":"10.1007","volume":"56","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7079-0472","authenticated-orcid":false,"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7280-6578","authenticated-orcid":false,"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5090-1769","authenticated-orcid":false,"given":"Dogan","family":"Ulus","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,1,7]]},"reference":[{"key":"327_CR1","doi-asserted-by":"crossref","unstructured":"Allan C, Avgustinov P, Christensen AS, Hendren LJ, Kuzins S, Lhotak O, de Moor O, Sereni D, Sittampalam G, Tibble J (2005) Adding trace matching with free variables to AspectJ. In: OOPSLA, pp 345\u2013364","DOI":"10.1145\/1094811.1094839"},{"issue":"3","key":"327_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2(3):117\u2013126","journal-title":"Distrib Comput"},{"key":"327_CR3","doi-asserted-by":"crossref","unstructured":"Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification, VMCAI, LNCS Volume 2937. Springer","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"327_CR4","doi-asserted-by":"crossref","unstructured":"Barringer H, Havelund K (2011) TraceContract: a scala DSL for trace analysis. In: Proceedings of the 17th international symposium on formal methods (FM\u201911), LNCS volume 6664. Springer","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"327_CR5","unstructured":"Barringer H, Rydeheard D, Havelund K (2007) Rule systems for run-time monitoring: from Eagle to RuleR. In: Proceedings of the 7th international workshop on runtime verification (RV\u201907), LNCS volume 4839. Springer"},{"issue":"2","key":"327_CR6","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin DA, Klaedtke F, M\u00fcller S, Zalinescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):45","journal-title":"J ACM"},{"key":"327_CR7","doi-asserted-by":"crossref","unstructured":"Bensalem S, Havelund K (2006) Dynamic deadlock analysis of multi-threaded programs. In: Haifa verification conference, Haifa, Israel, LNCS volume 3875. Springer","DOI":"10.1007\/11678779_15"},{"issue":"2","key":"327_CR8","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1109\/12.73590","volume":"40","author":"RE Bryant","year":"1991","unstructured":"Bryant RE (1991) On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans Comput 40(2):205\u2013213","journal-title":"IEEE Trans Comput"},{"issue":"3","key":"327_CR9","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant RE (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293\u2013318","journal-title":"ACM Comput Surv"},{"key":"327_CR10","doi-asserted-by":"publisher","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1990) Symbolic model checking: $$10^{20}$$ states and beyond. In: Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 428\u2013439. https:\/\/doi.org\/10.1109\/LICS.1990.113767","DOI":"10.1109\/LICS.1990.113767"},{"key":"327_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo B, Sankaranarayanan S, S\u00e1nchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: runtime monitoring of synchronous systems. In: TIME, pp 166\u2013174","DOI":"10.1109\/TIME.2005.26"},{"issue":"2","key":"327_CR12","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 (2016) Monitoring modulo theories. J Softw Tools Technol Transf 18(2):205\u2013225","journal-title":"J Softw Tools Technol Transf"},{"key":"327_CR13","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq J, Olivain J (2008) A Smell of ORCHIDS. In: Proceedings of the 8th international workshop on runtime verification (RV\u201908), LNCS volume 5289. Springer","DOI":"10.1007\/978-3-540-89247-2_1"},{"issue":"2","key":"327_CR14","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Hall\u00e9","year":"2012","unstructured":"Hall\u00e9 S, Villemaire R (2012) Runtime enforcement of web service message contracts with data. IEEE Trans Serv Comput 5(2):192\u2013206","journal-title":"IEEE Trans Serv Comput"},{"issue":"2","key":"327_CR15","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10009-014-0309-2","volume":"17","author":"K Havelund","year":"2015","unstructured":"Havelund K (2015) Rule-based runtime verification revisited. J Softw Tools Technol Transf 17(2):143\u2013170","journal-title":"J Softw Tools Technol Transf"},{"key":"327_CR16","doi-asserted-by":"crossref","unstructured":"Havelund K, Peled D, Ulus D (2017) First-order temporal logic monitoring with BDDs. In: 17th conference on formal methods in computer-aided design (FMCAD 2017), 2\u20136 Oct, 2017. IEEE, Vienna","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"327_CR17","doi-asserted-by":"crossref","unstructured":"Havelund K, Reger G, Thoma D, Z\u0103linescu E (2018) Monitoring events that carry data. In: Bartocci E, Falcone Y (eds) Lectures on runtime verification-introductory and advanced topics, LNCS volume 10457. Springer","DOI":"10.1007\/978-3-319-75632-5_3"},{"key":"327_CR18","doi-asserted-by":"crossref","unstructured":"Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. In: TACAS, pp 342\u2013356","DOI":"10.1007\/3-540-46002-0_24"},{"key":"327_CR19","doi-asserted-by":"crossref","unstructured":"Henriksen JG, Jensen JL, Jorgensen ME, Klarlund N, Paige R, Rauhe T, Sandholm A (1995) Mona: monadic second-order logic in practice. In: TACAS, pp 89\u2013110","DOI":"10.1007\/3-540-60630-0_5"},{"key":"327_CR20","unstructured":"JavaBDD. http:\/\/javabdd.sourceforge.net"},{"key":"327_CR21","unstructured":"Kim M, Kannan S, Lee I, Sokolsky O (2001) Java-MaC: a run-time assurance tool for Java. In: Proceedings of the 1st international workshop on runtime verification (RV\u201901), ENTCS, 55(2). Elsevier"},{"issue":"3","key":"327_CR22","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman O, Vardi MY (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291\u2013314","journal-title":"Form Methods Syst Des"},{"key":"327_CR23","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z Manna","year":"1991","unstructured":"Manna Z, Pnueli A (1991) Completing the temporal picture. Theor Comput Sci 83:91\u2013130","journal-title":"Theor Comput Sci"},{"key":"327_CR24","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith PO, Jin D, Griffith D, Chen F, Rosu G (2011) An overview of the MOP runtime verification framework. J Softw Tools Technol Transf 14:249\u2013289","journal-title":"J Softw Tools Technol Transf"},{"key":"327_CR25","doi-asserted-by":"crossref","unstructured":"Reger G, Cruz H, Rydeheard D (2015) MarQ: monitoring at runtime with QEA. In: Proceedings of the 21st international conference on tools and algorithms for the construction and analysis of systems (TACAS 2015). Springer","DOI":"10.1007\/978-3-662-46681-0_55"},{"issue":"4","key":"327_CR26","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/265924.265927","volume":"15","author":"S Savage","year":"1997","unstructured":"Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T (1997) Eraser: a dynamic data race detector for multithreaded programs. ACM Trans Comput Syst 15(4):391\u2013411","journal-title":"ACM Trans Comput Syst"},{"key":"327_CR27","doi-asserted-by":"crossref","unstructured":"Whaley J, Avots D, Carbin M, Lam MS (2005) Using Datalog with binary decision diagrams for program analysis. In: APLAS, pp 97\u2013118","DOI":"10.1007\/11575467_8"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00327-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-00327-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-00327-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,23]],"date-time":"2021-02-23T17:00:46Z","timestamp":1614099646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-00327-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,7]]},"references-count":27,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["327"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-00327-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,7]]},"assertion":[{"value":"7 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}