{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:04Z","timestamp":1762459624334},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319941103"},{"type":"electronic","value":"9783319941110"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94111-0_2","type":"book-chapter","created":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:07:44Z","timestamp":1529075264000},"page":"26-47","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Efficient Runtime Verification of First-Order Temporal Properties"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,6,16]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhotak, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: OOPSLA 2005, pp. 345\u2013364. IEEE (2005)","DOI":"10.1145\/1094811.1094839"},{"issue":"3","key":"2_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: TIME 2005, pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"2_CR4","unstructured":"Apache Commons CSV parser. \nhttps:\/\/commons.apache.org\/proper\/commons-csv"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44\u201357. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24622-0_5"},{"key":"2_CR6","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-21437-0_7"},{"key":"2_CR7","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-77395-5_10"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/2699444","volume":"62","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 45 (2015)","journal-title":"J. ACM"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-40787-1_4","volume-title":"Runtime Verification","author":"A Bauer","year":"2013","unstructured":"Bauer, A., K\u00fcster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59\u201375. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-40787-1_4"},{"issue":"3","key":"2_CR10","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"2_CR11","unstructured":"Cormen, Th.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. The MIT Press and McGraw-Hill Book Company (1989)"},{"issue":"2","key":"2_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/210197.210200","volume":"20","author":"J Chomicki","year":"1995","unstructured":"Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst. 20(2), 149\u2013186 (1995)","journal-title":"ACM Trans. Database Syst."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: LARVA - safer monitoring of real-time Java programs (tool paper), 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM), Hanoi, Vietnam, pp. 33\u201337. IEEE Computer Society (2009)","DOI":"10.1109\/SEFM.2009.13"},{"issue":"2","key":"2_CR14","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. J. Softw. Tools Technol. Transf. 18(2), 205\u2013225 (2016)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-89247-2_1","volume-title":"Runtime Verification","author":"J Goubault-Larrecq","year":"2008","unstructured":"Goubault-Larrecq, J., Olivain, J.: A smell of ORCHIDS. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 1\u201320. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-89247-2_1"},{"issue":"2","key":"2_CR16","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.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192\u2013206 (2012)","journal-title":"IEEE Trans. Serv. Comput."},{"issue":"2","key":"2_CR17","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. J. Softw. Tools Technol. Transf. 17(2), 143\u2013170 (2015)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. In: FMCAD 2017, pp. 116\u2013123. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102249"},{"key":"2_CR19","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-75632-5_3"},{"key":"2_CR20","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). \nhttps:\/\/doi.org\/10.1007\/3-540-46002-0_24"},{"key":"2_CR21","unstructured":"JavaBDD. \nhttp:\/\/javabdd.sourceforge.net"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). \nhttps:\/\/doi.org\/10.1007\/3-540-60630-0_5"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance tool for Java. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001). ENTCS, vol. 55(2). Elsevier (2001)","DOI":"10.1016\/S1571-0661(04)00254-3"},{"issue":"2","key":"2_CR24","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR25","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.: Completing the temporal picture. Theor. Comput. Sci. 83, 91\u2013130 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR26","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2012","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. J. Softw. Tools Technol. Transf. 14, 249\u2013289 (2012)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"2_CR27","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). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46681-0_55"},{"key":"2_CR28","unstructured":"Scala Parser Combinators. \nhttps:\/\/github.com\/scala\/scala-parser-combinators"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/11575467_8","volume-title":"Programming Languages and Systems","author":"J Whaley","year":"2005","unstructured":"Whaley, J., Avots, D., Carbin, M., Lam, M.S.: Using Datalog with binary decision diagrams for program analysis. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 97\u2013118. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11575467_8"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94111-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,6,15]],"date-time":"2018-06-15T15:08:49Z","timestamp":1529075329000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94111-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319941103","9783319941110"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94111-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}