{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:06:22Z","timestamp":1784844382974,"version":"3.55.0"},"publisher-location":"Cham","reference-count":80,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319919072","type":"print"},{"value":"9783319919089","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-319-91908-9_25","type":"book-chapter","created":{"date-parts":[[2019,10,4]],"date-time":"2019-10-04T05:05:00Z","timestamp":1570165500000},"page":"532-562","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Runtime Verification Past Experiences and Future Projections"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Havelund","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,5]]},"reference":[{"key":"25_CR1","doi-asserted-by":"publisher","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."},{"issue":"1","key":"25_CR2","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/565816.503275","volume":"37","author":"G Ammons","year":"2002","unstructured":"Ammons, G., Bod\u00edk, R., Larus, J.R.: Mining specifications. ACM Sigplan Not. 37(1), 4\u201316 (2002)","journal-title":"ACM Sigplan Not."},{"issue":"4","key":"25_CR3","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1002\/stvr.281","volume":"13","author":"C Artho","year":"2004","unstructured":"Artho, C., Havelund, K., Biere, A.: High-level data races. Softw. Test. Verification Reliab. 13(4), 207\u2013227 (2004)","journal-title":"Softw. Test. Verification Reliab."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Artho, C., Havelund, K., Honiden, S.: Visualization of concurrent program executions. In: 31st Annual International Computer Software and Applications Conference (COMPSAC 2007), vol. 2, pp. 541\u2013546, July 2007","DOI":"10.1109\/COMPSAC.2007.236"},{"key":"25_CR5","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-32759-9_9"},{"key":"25_CR6","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24622-0_5"},{"issue":"11","key":"25_CR7","doi-asserted-by":"publisher","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.: Formal analysis of log files. J. Aerospace Comput. Inf. Commun. 7(11), 365\u2013390 (2010)","journal-title":"J. Aerospace Comput. Inf. Commun."},{"key":"25_CR8","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-21437-0_7"},{"issue":"3","key":"25_CR9","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1093\/logcom\/exn076","volume":"20","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Logic Comput. 20(3), 675\u2013706 (2010)","journal-title":"J. Logic Comput."},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-75632-5_1","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1\u201333. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-75632-5_1"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-35632-2_18","volume-title":"Runtime Verification","author":"E Bartocci","year":"2013","unstructured":"Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168\u2013182. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-35632-2_18"},{"key":"25_CR12","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-77395-5_11"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/11901433_41","volume-title":"Formal Methods and Software Engineering","author":"A Bauer","year":"2006","unstructured":"Bauer, A., Leucker, M., Streit, J.: SALT\u2014structured assertion language for temporal logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 757\u2013775. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11901433_41"},{"issue":"11","key":"25_CR14","doi-asserted-by":"publisher","first-page":"338","DOI":"10.2514\/1.40331","volume":"7","author":"M Bennett","year":"2010","unstructured":"Bennett, M., Borgen, R., Havelund, K., Ingham, M., Wagner, D.: Prototyping a domain-specific language for monitor and control systems. J. Aerospace Comput. Inf. Commun. 7(11), 338\u2013364 (2010)","journal-title":"J. Aerospace Comput. Inf. Commun."},{"key":"25_CR15","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). \n                      https:\/\/doi.org\/10.1007\/11678779_15"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-29860-8_28","volume-title":"Runtime Verification","author":"E Bodden","year":"2012","unstructured":"Bodden, E.: MOPBox: a library approach to runtime verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 365\u2013369. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-29860-8_28"},{"issue":"4","key":"25_CR17","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TSE.2010.25","volume":"36","author":"E Bodden","year":"2010","unstructured":"Bodden, E., Havelund, K.: Aspect-oriented race detection in Java. IEEE Trans. Softw. Eng. 36(4), 509\u2013527 (2010)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"25_CR18","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/978-3-319-91908-9_24","volume-title":"Computing and Software Science","author":"G Candea","year":"2018","unstructured":"Candea, G., Godefroid, P.: Automated software test generation: some challenges, solutions, and recent advances. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 505\u2013531. Springer, Heidelberg (2018)"},{"issue":"4","key":"25_CR19","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s004460050049","volume":"11","author":"CM Chase","year":"1998","unstructured":"Chase, C.M., Garg, V.K.: Detection of global predicates: techniques and their limitations. Distrib. Comput. 11(4), 191\u2013201 (1998)","journal-title":"Distrib. Comput."},{"key":"25_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-319-91908-9_15","volume-title":"Computing and Software Science","author":"R Chatley","year":"2018","unstructured":"Chatley, R., Donaldson, A., Mycroft, A.: The next 7000 programming languages. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 250\u2013282. Springer, Heidelberg (2018)"},{"key":"25_CR21","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-30482-1_31","volume-title":"Formal Methods and Software Engineering","author":"Feng Chen","year":"2004","unstructured":"Chen, F., D\u2019Amorim, M., Ro\u015fu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 357\u2013372. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-30482-1_31"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Chen, F., Ro\u015fu, G.: Towards monitoring-oriented programming: a paradigm combining specification and implementation. In: Proceedings of the 3rd International Workshop on Runtime Verification (RV 2003). Electronic Notes in Theoretical Computer Science, vol. 89, no. 2, pp. 108\u2013127. Elsevier Science Inc. (2003)","DOI":"10.1016\/S1571-0661(04)81045-4"},{"key":"25_CR23","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 (2007). ACM SIGPLAN Notices"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-73368-3_27","volume-title":"Computer Aided Verification","author":"F Chen","year":"2007","unstructured":"Chen, F., Ro\u015fu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 240\u2013253. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-73368-3_27"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Chen, F., Serbanuta, T.F., Rosu, G.: jPredictor: a predictive runtime analysis tool for Java. In: ICSE (2008)","DOI":"10.1145\/1368088.1368119"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Cooper, R., Marzullo, K.: Consistent detection of global predicates. ACM SIGPLAN Not. 26(12), 167\u2013174 (1991). Proceedings of the ACM\/ONR Workshop on Parallel and Distributed Debugging","DOI":"10.1145\/127695.122774"},{"issue":"4","key":"25_CR27","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. Notes 30(4), 1\u20137 (2005)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"De la Higuera, C.: Grammatical inference: learning automata and grammars. Cambridge University Press, Cambridge (2010)","DOI":"10.1017\/CBO9781139194655"},{"key":"25_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-642-54862-8_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Decker","year":"2014","unstructured":"Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 341\u2013356. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54862-8_23"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/10722468_19","volume-title":"SPIN Model Checking and Software Verification","author":"D Drusinsky","year":"2000","unstructured":"Drusinsky, D.: The temporal rover and the ATG rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323\u2013330. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10722468_19"},{"issue":"3","key":"25_CR31","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/s10009-011-0196-8","volume":"14","author":"Y Falcone","year":"2012","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Trans. 14(3), 349\u2013382 (2012)","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"25_CR32","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. 34, pp. 141\u2013175. IOS Press (2013)"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Fidge, C.J.: Partial orders for parallel debugging. In: Proceedings of the 1988 ACM SIGPLAN and SIGOPS Workshop on Parallel and Distributed debugging, pp. 183\u2013194. ACM (1988)","DOI":"10.1145\/68210.69233"},{"key":"25_CR34","unstructured":"Filman, R., Havelund, K.: Source-code instrumentation and quantification of events. In: Foundations of Aspect-Oriented Languages (FOAL 2002), Enschede, The Netherlands, April 2002"},{"issue":"3","key":"25_CR35","doi-asserted-by":"publisher","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":"25_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/10722468_20","volume-title":"SPIN Model Checking and Software Verification","author":"JJ Harrow","year":"2000","unstructured":"Harrow, J.J.: Runtime checking of multithreaded applications with visual threads. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 331\u2013342. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10722468_20"},{"key":"25_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10722468_15","volume-title":"SPIN Model Checking and Software Verification","author":"K Havelund","year":"2000","unstructured":"Havelund, K.: Using runtime analysis to guide model checking of Java programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 245\u2013264. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10722468_15"},{"key":"25_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-540-68524-1_3","volume-title":"Testing of Software and Communicating Systems","author":"K Havelund","year":"2008","unstructured":"Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) FATES\/TestCom -2008. LNCS, vol. 5047, pp. 7\u201322. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-68524-1_3"},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Havelund, K.: Data automata in Scala. In: Proceedings of the 8th International Symposium on Theoretical Aspects of Software Engineering (TASE 2014). IEEE Computer Society (2014)","DOI":"10.1109\/TASE.2014.37"},{"issue":"2","key":"25_CR40","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. Int. J. Softw. Tools Technol. Trans. 17(2), 143\u2013170 (2015)","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"25_CR41","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-69149-5_40"},{"key":"25_CR42","doi-asserted-by":"crossref","unstructured":"Havelund, K., Peled, D.A., Ulus, D.: First order temporal logic monitoring with BDDs. In: Formal Methods in Computer Aided Design (FMCAD), pp. 116\u2013123. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102249"},{"issue":"4","key":"25_CR43","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"25_CR44","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-658-09994-7_6","volume-title":"Formal Modeling and Verification of Cyber-Physical Systems","author":"K Havelund","year":"2015","unstructured":"Havelund, K., Reger, G.: Specification of parametric monitors. In: Drechsler, R., K\u00fchne, U. (eds.) Formal Modeling and Verification of Cyber-Physical Systems, pp. 151\u2013189. Springer, Wiesbaden (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-658-09994-7_6"},{"key":"25_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-319-63121-9_16","volume-title":"Models, Algorithms, Logics and Tools","author":"K Havelund","year":"2017","unstructured":"Havelund, K., Reger, G.: Runtime verification logics - a language design perspective. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 310\u2013338. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63121-9_16"},{"key":"25_CR46","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-75632-5_3"},{"issue":"2","key":"25_CR47","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/B:FORM.0000017721.39909.4b","volume":"24","author":"K Havelund","year":"2004","unstructured":"Havelund, K., Ro\u015fu, G.: An overview of the runtime verification tool Java PathExplorer. Formal Methods Syst. Des. 24(2), 189\u2013215 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR48","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), pp. 135\u2013143 (2001)"},{"issue":"1","key":"25_CR49","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/s10009-002-0080-7","volume":"4","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Visser, W.: Program model checking as a new trend. STTT 4(1), 8\u201320 (2002)","journal-title":"STTT"},{"key":"25_CR50","unstructured":"Havelund, K., Wyk, E.V.: Aspect-oriented monitoring of C programs. In: The Sixth IARP-IEEE\/RAS-EURON Joint Workshop on Technical Challenges for Dependable Robots in Human Environments, Pasadena, CA, 17\u201318 May 2008"},{"key":"25_CR51","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/978-3-319-91908-9_26","volume-title":"Computing and Software Science","author":"F Howar","year":"2018","unstructured":"Howar, F., Jonsson, B., Vaandrager, F.: Combining black-box and white-box techniques for learning register automata. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 563\u2013588. Springer, Heidelberg (2018)"},{"key":"25_CR52","doi-asserted-by":"crossref","unstructured":"Huang, J., Meredith, P., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. In: Proceedings of the 35th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2014), pp. 337\u2013348. ACM, June 2014","DOI":"10.1145\/2666356.2594315"},{"issue":"1\u20132","key":"25_CR53","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10994-013-5419-7","volume":"96","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: Learning register automata: from languages to program structures. Mach. Learn. 96(1\u20132), 65\u201398 (2014)","journal-title":"Mach. Learn."},{"key":"25_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-11164-3_26","volume-title":"Runtime Verification","author":"M Isberner","year":"2014","unstructured":"Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307\u2013322. Springer, Cham (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-319-11164-3_26"},{"key":"25_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/978-3-319-21690-4_32","volume-title":"Computer Aided Verification","author":"M Isberner","year":"2015","unstructured":"Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487\u2013495. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21690-4_32"},{"key":"25_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-319-46982-9_15","volume-title":"Runtime Verification","author":"S Kauffman","year":"2016","unstructured":"Kauffman, S., Havelund, K., Joshi, R.: nfer \u2013 a notation and system for inferring event stream abstractions. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 235\u2013250. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-46982-9_15"},{"key":"25_CR57","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). \n                      https:\/\/doi.org\/10.1007\/3-540-45337-7_18"},{"key":"25_CR58","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-47166-2_1"},{"key":"25_CR59","doi-asserted-by":"crossref","unstructured":"Lee, C., Chen, F., Rosu, G.: Mining parametric specifications. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, 21\u201328 May 2011, Waikiki, Honolulu, HI, USA, pp. 591\u2013600 (2011)","DOI":"10.1145\/1985793.1985874"},{"key":"25_CR60","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and Software Science","author":"A Legay","year":"2018","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478\u2013504. Springer, Heidelberg (2018)"},{"key":"25_CR61","doi-asserted-by":"crossref","unstructured":"Lo, D., Khoo, S.-C., Han, J., Liu, C.: Mining Software Specifications: Methodologies and Applications. CRC Press, Boca Raton (2011)","DOI":"10.1201\/b10928"},{"key":"25_CR62","unstructured":"Mattern, F.: Virtual time and global states of distributed systems. In: Cosnard, M., et al. (eds.) Parallel and Distributed Algorithms: Proceedings of the International Workshop on Parallel and Distributed Algorithms, pp. 215\u2013226. Elsevier Science (1989)"},{"key":"25_CR63","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"P Meredith","year":"2011","unstructured":"Meredith, P., Jin, D., Griffith, D., Chen, F., Ro\u015fu, G.: An overview of the MOP runtime verification framework. J. Softw. Tools Technol. Transf. 14, 249\u2013289 (2011)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"25_CR64","doi-asserted-by":"crossref","unstructured":"Reger, G., Barringer, H., Rydeheard, D.: A pattern-based approach to parametric specification mining. In: 2013 IEEE\/ACM 28th International Conference on Automated Software Engineering (ASE), pp. 658\u2013663, November 2013","DOI":"10.1109\/ASE.2013.6693129"},{"key":"25_CR65","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). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46681-0_55"},{"issue":"1","key":"25_CR66","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(1:9)2012","volume":"8","author":"G Ro\u015fu","year":"2012","unstructured":"Ro\u015fu, G., Chen, F.: Semantics and algorithms for parametric monitoring. Logical Methods Comput. Sci. 8(1), 1\u201347 (2012)","journal-title":"Logical Methods Comput. Sci."},{"key":"25_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-20398-5_23","volume-title":"NASA Formal Methods","author":"M Said","year":"2011","unstructured":"Said, M., Wang, C., Yang, Z., Sakallah, K.: Generating data race witnesses by an SMT-based analysis. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 313\u2013327. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-20398-5_23"},{"issue":"4","key":"25_CR68","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.: Eraser: a dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391\u2013411 (1997)","journal-title":"ACM Trans. Comput. Syst."},{"key":"25_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-540-24730-2_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Sen","year":"2004","unstructured":"Sen, K., Ro\u015fu, G., Agha, G.: Online efficient predictive safety analysis of multithreaded programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 123\u2013138. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24730-2_9"},{"key":"25_CR70","doi-asserted-by":"crossref","unstructured":"Sen, K., Rosu, G., Agha, G.: Runtime safety analysis of multithreaded programs. In: Proceedings of ESEC\/FSE 2003: European Software Engineering Conference and ACM SIGSOFT International Symposium on the Foundations of Software Engineering. ACM, Helsinki, September 2003","DOI":"10.1145\/940071.940116"},{"key":"25_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/11494881_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"K Sen","year":"2005","unstructured":"Sen, K., Ro\u015fu, G., Agha, G.: Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 211\u2013226. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11494881_14"},{"key":"25_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-35632-2_16","volume-title":"Runtime Verification","author":"TF \u015eerb\u0103nu\u0163\u0103","year":"2013","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Chen, F., Ro\u015fu, G.: Maximal causal models for sequentially consistent systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 136\u2013150. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-35632-2_16"},{"issue":"3","key":"25_CR73","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10703-012-0171-3","volume":"41","author":"J Seyster","year":"2012","unstructured":"Seyster, J., Dixit, K., Huang, X., Grosu, R., Havelund, K., Smolka, S.A., Stoller, S.D., Zadok, E.: InterAspect: aspect-oriented instrumentation with GCC. Formal Methods Syst. Des. 41(3), 295\u2013320 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR74","unstructured":"Smith, D.R., Havelund, K.: Toward automated enforcement of error-handling policies. Technical report number: TR-KT-0508, Kestrel Technology LLC, August 2005"},{"key":"25_CR75","unstructured":"Smith, M.H., Holzmann, G.J., Etessami, K.: Events and constraints: a graphical editor for capturing logic requirements of programs. In: 21st IEEE International Requirements Engineering Conference (RE), Toronto, Canada, August 2001"},{"key":"25_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/BFb0030684","volume-title":"Distributed Algorithms","author":"SD Stoller","year":"1997","unstructured":"Stoller, S.D.: Detecting global predicates in distributed systems with clocks. In: Mavronicolas, M., Tsigas, P. (eds.) WDAG 1997. LNCS, vol. 1320, pp. 185\u2013199. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/BFb0030684"},{"key":"25_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-29860-8_15","volume-title":"Runtime Verification","author":"SD Stoller","year":"2012","unstructured":"Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193\u2013207. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-29860-8_15"},{"key":"25_CR78","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). Electronic Notes in Theoretical Computer Science, vol. 144, no. 4, pp. 109\u2013124. Elsevier Science Inc. (2006)","DOI":"10.1016\/j.entcs.2006.02.007"},{"key":"25_CR79","doi-asserted-by":"crossref","unstructured":"Stolz, V., Huch, F.: Runtime verification of concurrent Haskell programs. In: Proceedings of the 4th International Workshop on Runtime Verification (RV 2004). Electronic Notes in Theoretical Computer Science, vol. 113, pp. 201\u2013216. Elsevier Science Inc. (2005)","DOI":"10.1016\/j.entcs.2004.01.026"},{"key":"25_CR80","doi-asserted-by":"crossref","unstructured":"Walker, R., Viggers, K.: Implementing protocols via declarative event patterns. In: Taylor, R., Dwyer, M. (eds.) ACM Sigsoft 12th International Symposium on Foundations of Software Engineering (FSE-12), pp. 159\u2013169. ACM Press (2004)","DOI":"10.1145\/1029894.1029918"}],"container-title":["Lecture Notes in Computer Science","Computing and Software Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-91908-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T20:03:16Z","timestamp":1570305796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-91908-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783319919072","9783319919089"],"references-count":80,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-91908-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}