{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:09Z","timestamp":1773827469286,"version":"3.50.1"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319631202","type":"print"},{"value":"9783319631219","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63121-9_16","type":"book-chapter","created":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T08:05:15Z","timestamp":1500883515000},"page":"310-338","source":"Crossref","is-referenced-by-count":19,"title":["Runtime Verification Logics A Language Design Perspective"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"key":"16_CR1","unstructured":"XTL Manual. http:\/\/cadp.inria.fr\/man\/xtl.html"},{"key":"16_CR2","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1145\/1103845.1094839","volume":"40","author":"C Allan","year":"2005","unstructured":"Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhot\u00e1k, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. SIGPLAN Not. 40, 345\u2013364 (2005)","journal-title":"SIGPLAN Not."},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-32759-9_9","volume-title":"FM 2012: Formal Methods","author":"H Barringer","year":"2012","unstructured":"Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68\u201384. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32759-9_9"},{"key":"16_CR4","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). doi: 10.1007\/978-3-540-24622-0_5"},{"key":"16_CR5","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). doi: 10.1007\/978-3-642-21437-0_7"},{"issue":"3","key":"16_CR6","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. 20(3), 675\u2013706 (2010)","journal-title":"J. Log. Comput."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass - Java with assertions. In: Proceedings of the 1st International Workshop on Runtime Verification (RV 2001), Paris, France, ENTCS, vol. 55, no. 2, pp. 103\u2013117. Elsevier, July 2001. http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.92.144&rep=rep1&type=pdf","DOI":"10.1016\/S1571-0661(04)00247-6"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Proceedings of the Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, 22\u201325 September 2014, pp. 1\u20139 (2014)","DOI":"10.1007\/978-3-319-11164-3_1"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf. 1\u201340 (2017). https:\/\/link.springer.com\/article\/10.1007%2Fs10009-017-0454-5","DOI":"10.1007\/s10009-017-0454-5"},{"key":"16_CR10","doi-asserted-by":"crossref","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, 262\u2013285 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR11","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: Proceedings of the 28th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), vol. 2, pp. 49\u201360. Schloss Dagstuhl - Leibniz Center for Informatics (2008)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-03466-4_6","volume-title":"Theoretical Aspects of Computing - ICTAC 2009","author":"A Bauer","year":"2009","unstructured":"Bauer, A., Gor\u00e9, R., Tiu, A.: A first-order policy language for history-based transaction monitoring. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 96\u2013111. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-03466-4_6"},{"issue":"3","key":"16_CR13","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/s10703-015-0227-2","volume":"46","author":"A Bauer","year":"2015","unstructured":"Bauer, A., K\u00fcster, J., Vegliach, G.: The ins and outs of first-order runtime verification. Formal Methods Syst. Des. 46(3), 286\u2013316 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-77395-5_11","volume-title":"Runtime Verification","author":"A Bauer","year":"2007","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126\u2013138. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-77395-5_11"},{"issue":"4","key":"16_CR15","doi-asserted-by":"crossref","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/11678779_15","volume-title":"Hardware and Software, Verification and Testing","author":"S Bensalem","year":"2006","unstructured":"Bensalem, S., Havelund, K.: Dynamic deadlock analysis of multi-threaded programs. In: Ur, S., Bin, E., Wolfsthal, Y. (eds.) HVC 2005. LNCS, vol. 3875, pp. 208\u2013223. Springer, Heidelberg (2006). doi: 10.1007\/11678779_15"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-35861-6_4","volume-title":"Formal Aspects of Component Software","author":"D Bianculli","year":"2013","unstructured":"Bianculli, D., Ghezzi, C., San Pietro, P.: The tale of SOLOIST: a specification language for service compositions interactions. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 55\u201372. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35861-6_4"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Chen, F., Ro\u015fu, G.: MOP: an efficient and generic runtime verification framework. In: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2007), pp. 569\u2013588. ACM Press (2007)","DOI":"10.1145\/1297027.1297069"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Cheng, K.T., Krishnakumar, A.S.: Automatic functional test generation using the extended finite state machine model. In: Proceedings of the 30th International Design Automation Conference, DAC 1993, pp. 86\u201391. ACM, New York (1993)","DOI":"10.1145\/157485.164585"},{"issue":"2","key":"16_CR20","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1145\/383891.383892","volume":"26","author":"J Chomicki","year":"2001","unstructured":"Chomicki, J., Toman, D., B\u00f6hlen, M.H.: Querying ATSQL databases with temporal logic. ACM Trans. Database Syst. 26(2), 145\u2013178 (2001)","journal-title":"ACM Trans. Database Syst."},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). doi: 10.1007\/BFb0025774"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: LARVA \u2013 safer monitoring of real-time Java programs (tool paper). In: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, pp. 33\u201337. IEEE Computer Society, Washington, DC (2009)","DOI":"10.1109\/SEFM.2009.13"},{"key":"16_CR23","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: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, pp. 166\u2013174. IEEE Computer Society (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-38088-4_34","volume-title":"NASA Formal Methods","author":"N Decker","year":"2013","unstructured":"Decker, N., Leucker, M., Thoma, D.: jUnitRV\u2013adding runtime verification to jUnit. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 459\u2013464. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38088-4_34"},{"key":"16_CR25","first-page":"1","volume":"18","author":"N Decker","year":"2015","unstructured":"Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18, 1\u201321 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"16_CR26","doi-asserted-by":"crossref","first-page":"16:1","DOI":"10.1145\/1507244.1507246","volume":"10","author":"S Demri","year":"2009","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3), 16:1\u201316:30 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"16_CR27","unstructured":"Drusinsky, D.: Modeling and Verification using UML Statecharts, 400 p. Elsevier, Amsterdam (2006). ISBN-13: 978-0-7506-7949-7"},{"key":"16_CR28","unstructured":"Eisner, C., Fisman, D.: Temporal logic made practical. In: Handbook of Model Checking (2014, to appear). http:\/\/www.cis.upenn.edu\/~fisman\/publications.html"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, vol. B, pp. 995\u20131072. MIT Press, Cambridge (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-04694-0_4","volume-title":"Runtime Verification","author":"Y Falcone","year":"2009","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40\u201359. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04694-0_4"},{"key":"16_CR31","first-page":"141","volume":"34","author":"Y Falcone","year":"2013","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Eng. Dependable Softw. Syst. 34, 141\u2013175 (2013)","journal-title":"Eng. Dependable Softw. Syst."},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-23820-3_27","volume-title":"Runtime Verification","author":"Y Falcone","year":"2015","unstructured":"Falcone, Y., Ni\u010dkovi\u0107, D., Reger, G., Thoma, D.: Second international competition on runtime verification. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 405\u2013422. Springer, Cham (2015). doi: 10.1007\/978-3-319-23820-3_27"},{"issue":"3","key":"16_CR33","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/s10703-005-3399-3","volume":"27","author":"B Finkbeiner","year":"2005","unstructured":"Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime executions. Formal Methods Syst. Des. 27(3), 253\u2013274 (2005)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR34","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-36742-7_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Grigore","year":"2013","unstructured":"Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 260\u2013276. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_19"},{"issue":"2","key":"16_CR36","doi-asserted-by":"crossref","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":"16_CR37","doi-asserted-by":"crossref","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. Int. J. Softw. Tools Technol. Transf. 17(2), 143\u2013170 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"16_CR38","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/s10009-003-0117-6","volume":"6","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6(2), 158\u2013173 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"16_CR39","volume-title":"The SPIN Model Checker","author":"G Holzmann","year":"2004","unstructured":"Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Boston (2004)"},{"issue":"2","key":"16_CR40","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theoret. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"16_CR41","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). doi: 10.1007\/3-540-45337-7_18"},{"issue":"2","key":"16_CR42","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"M Kim","year":"2004","unstructured":"Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Formal Methods Syst. Des. 24(2), 129\u2013155 (2004)","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"16_CR43","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. Theoret. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"16_CR44","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"16_CR45","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, pp. 383\u2013392. IEEE Computer Society, Washington, DC (2002)","DOI":"10.1109\/LICS.2002.1029846"},{"key":"16_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-47166-2_1","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"KG Larsen","year":"2016","unstructured":"Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 3\u201315. Springer, Cham (2016). doi: 10.1007\/978-3-319-47166-2_1"},{"key":"16_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16612-9_11"},{"issue":"5","key":"16_CR48","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293\u2013303 (2009)","journal-title":"J. Log. Algebr. Program."},{"key":"16_CR49","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York Inc. (1995)"},{"key":"16_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-319-46982-9_16","volume-title":"Runtime Verification","author":"R Medhat","year":"2016","unstructured":"Medhat, R., Bonakdarpour, B., Fischmeister, S., Joshi, Y.: Accelerated runtime verification of LTL specifications with counting semantics. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 251\u2013267. Springer, Cham (2016). doi: 10.1007\/978-3-319-46982-9_16"},{"key":"16_CR51","first-page":"1","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Ro\u015fu, G.: An overview of the MOP runtime verification framework. J. Softw. Tools Technol. Transf. 14, 1\u201341 (2011)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"16_CR52","unstructured":"OMG. OMG Unified Modeling Language (OMG UML), Superstructure, Version 2.4.1, August 2011"},{"key":"16_CR53","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46\u201357. IEEE Computer Society, Washington, DC (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"16_CR54","unstructured":"Reger, G.: Automata based monitoring and mining of execution traces. Ph.D. thesis, University of Manchester (2014)"},{"key":"16_CR55","doi-asserted-by":"crossref","unstructured":"Reger, G., Cruz, H.C., Rydeheard, D.: 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) (2015)","DOI":"10.1007\/978-3-662-46681-0_55"},{"key":"16_CR56","doi-asserted-by":"crossref","unstructured":"Reger, G., Hall\u00e9, S., Falcone, Y.: Third international competition on runtime verification CRV 2016. In: Proceedings of the Runtime Verification - 16th International Conference, RV 2016 (2016)","DOI":"10.1007\/978-3-319-46982-9_3"},{"key":"16_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-319-23820-3_14","volume-title":"Runtime Verification","author":"G Reger","year":"2015","unstructured":"Reger, G., Rydeheard, D.: From first-order temporal logic to parametric trace slicing. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 216\u2013232. Springer, Cham (2015). doi: 10.1007\/978-3-319-23820-3_14"},{"key":"16_CR58","volume-title":"Introduction to the Theory of Computation","author":"M Sipser","year":"2013","unstructured":"Sipser, M.: Introduction to the Theory of Computation, 3rd edn. Cengage Learning, Boston (2013)","edition":"3"},{"key":"16_CR59","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), ENTCS, vol. 144, no. 4, pp. 109\u2013124. Elsevier (2006)","DOI":"10.1016\/j.entcs.2006.02.007"},{"issue":"1","key":"16_CR60","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"RE Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157\u2013171 (1986)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-69850-0_10","volume-title":"25 Years of Model Checking","author":"MY Vardi","year":"2008","unstructured":"Vardi, M.Y.: From church and prior to PSL. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 150\u2013171. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-69850-0_10"}],"container-title":["Lecture Notes in Computer Science","Models, Algorithms, Logics and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63121-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T13:29:19Z","timestamp":1569936559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63121-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631202","9783319631219"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63121-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}