{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T08:27:48Z","timestamp":1768638468806,"version":"3.49.0"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319471686","type":"print"},{"value":"9783319471693","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_25","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T21:56:23Z","timestamp":1475618183000},"page":"339-355","source":"Crossref","is-referenced-by-count":14,"title":["What Is a Trace? A Runtime Verification Perspective"],"prefix":"10.1007","author":[{"given":"Giles","family":"Reger","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"25_CR1","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":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). doi: 10.1007\/BFb0032042"},{"issue":"1","key":"25_CR3","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181\u2013203 (1994)","journal-title":"J. ACM"},{"issue":"2","key":"25_CR4","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1145\/506147.506151","volume":"49","author":"E Asarin","year":"2002","unstructured":"Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172\u2013206 (2002)","journal-title":"J. ACM"},{"key":"25_CR5","unstructured":"AspectC++. Aspect oriented programming for C++ (2016). http:\/\/www.aspectc.org"},{"key":"25_CR6","unstructured":"AspectJ. Aspect oriented programming for Java (2016). https:\/\/eclipse.org\/aspectj\/"},{"key":"25_CR7","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":"25_CR8","doi-asserted-by":"crossref","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: VMCAI, pp. 44\u201357 (2004)","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"25_CR9","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"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-11164-3_1","volume-title":"Runtime Verification","author":"E Bartocci","year":"2014","unstructured":"Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 1\u20139. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11164-3_1"},{"key":"25_CR11","unstructured":"Bartocci, E., Bonakdarpour, B., Falcone, Y., Colombo, C., Decker, N., Klaedtke, F., Havelund, K., Joshi, Y., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification. Int. J. Softw. Tools Technol. Transf. (STTT) (to appear, 2016)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-319-26916-0_9","volume-title":"Hybrid Systems Biology","author":"E Bartocci","year":"2015","unstructured":"Bartocci, E., Bortolussi, L., Milios, D., Nenzi, L., Sanguinetti, G.: Studying emergent behaviours in\u00a0morphogenesis using signal spatio-temporal\u00a0logic. In: Abate, A., \u0160afr\u00e1nek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 156\u2013172. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-26916-0_9"},{"key":"25_CR13","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). doi: 10.1007\/978-3-642-35632-2_18"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1007\/978-3-642-29860-8_27","volume-title":"Runtime Verification","author":"D Basin","year":"2012","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Z\u0103linescu, E.: Monpoly: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2012. LNCS, vol. 7186, pp. 360\u2013364. Springer, Berlin Heidelberg (2012)"},{"issue":"3","key":"25_CR15","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(3), 262\u2013285 (2015)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"25_CR16","doi-asserted-by":"crossref","first-page":"15:1","DOI":"10.1145\/2699444","volume":"62","author":"D Basin","year":"2015","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S., Z\u0103linescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1\u201315:45 (2015)","journal-title":"J. ACM"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27755-2_3"},{"key":"25_CR18","unstructured":"Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor-based systems. In: Proceedings of the 13th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems, FOCLASA 2014, Rome, Italy, 6th September 2014, pp. 54\u201368, 2014 (2014)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-33693-0_12","volume-title":"Integrated Formal Methods","author":"I Cassar","year":"2016","unstructured":"Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 176\u2013192. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-33693-0_12"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-00768-2_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Chen","year":"2009","unstructured":"Chen, F., Ro\u015fu, G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 246\u2013261. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00768-2_23"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-662-49674-9_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z Chen","year":"2016","unstructured":"Chen, Z., Wang, Z., Zhu, Y., Xi, H., Yang, Z.: Parametric runtime verification of C programs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 299\u2013315. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_17"},{"key":"25_CR22","unstructured":"CIL. C Intermediate Language (2016). https:\/\/www.cs.berkeley.edu\/~necula\/cil\/"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-29860-8_29","volume-title":"Runtime Verification","author":"C Colombo","year":"2012","unstructured":"Colombo, C., Francalanza, A., Gatt, R.: Elarva: a monitoring tool for Erlang. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 370\u2013374. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-29860-8_29"},{"key":"25_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":"25_CR25","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). doi: 10.1007\/978-3-642-54862-8_23"},{"issue":"3","key":"25_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1507244.1507246","volume":"10","author":"S Demri","year":"2009","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the freeze quantifier, register automata. ACM Trans. Comput. Logic 10(3), 1\u201330 (2009)","journal-title":"ACM Trans. Comput. Logic"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/978-3-642-33386-6_9","volume-title":"ATVA 2012","author":"A Donz\u00e9","year":"2012","unstructured":"Donz\u00e9, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92\u2013106. Springer, Heidelberg (2012)"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-09195-2_4","volume-title":"Modelling Foundations and Applications","author":"W Dou","year":"2014","unstructured":"Dou, W., Bianculli, D., Briand, L.: OCLR: a more expressive, pattern-based temporal extension of OCL. In: Cabot, J., Rubin, J. (eds.) ECMFA 2014. LNCS, vol. 8569, pp. 51\u201366. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-09195-2_4"},{"key":"25_CR29","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D. (eds.) Summer School Marktoberdorf 2012 - Engineering Dependable Software Systems. IOS Press (2013). to appear"},{"key":"25_CR30","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, Heidelberg (2015). doi: 10.1007\/978-3-319-23820-3_27"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Gol, E.A., Bartocci, E., Belta, C.: A formal methods approach to pattern synthesis in reaction diffusion systems. In: 53rd IEEE Conference on Decision and Control, pp. 108\u2013113, December 2014","DOI":"10.1109\/CDC.2014.7039367"},{"key":"25_CR32","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":"3","key":"25_CR33","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/1467247.1467271","volume":"52","author":"R Grosu","year":"2009","unstructured":"Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97\u2013105 (2009)","journal-title":"Commun. ACM"},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Gros, R., Belta, C.: Spatel: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, pp. 189\u2013198. ACM, New York (2015)","DOI":"10.1145\/2728606.2728633"},{"issue":"2","key":"25_CR35","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1109\/TSC.2011.10","volume":"5","author":"S Halle","year":"2012","unstructured":"Halle, 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."},{"key":"25_CR36","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). doi: 10.1007\/978-3-540-68524-1_3"},{"key":"25_CR37","unstructured":"Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003)"},{"issue":"6","key":"25_CR38","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1145\/2666356.2594315","volume":"49","author":"J Huang","year":"2014","unstructured":"Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. SIGPLAN Not. 49(6), 337\u2013348 (2014)","journal-title":"SIGPLAN Not."},{"key":"25_CR39","doi-asserted-by":"crossref","unstructured":"Jak\u0161i\u0107, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ni\u010dkovi\u00e9, D.: From signal temporal logic to FPGA monitors. In: 2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 218\u2013227, September 2015","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"25_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-40787-1_9","volume-title":"Runtime Verification","author":"K Kalajdzic","year":"2013","unstructured":"Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S.D., Grosu, R.: Runtime verification with particle filtering. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 149\u2013166. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40787-1_9"},{"issue":"2","key":"25_CR41","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. Theor. Comput. Sci. 134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"25_CR42","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1023\/B:FORM.0000017719.43755.7c","volume":"24","author":"MZ Kim","year":"2004","unstructured":"Kim, M.Z., 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."},{"key":"25_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-40787-1_10","volume-title":"Runtime Verification","author":"N Kosmatov","year":"2013","unstructured":"Kosmatov, N., Petiot, G., Signoles, J.: An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 167\u2013182. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40787-1_10"},{"issue":"4","key":"25_CR44","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","volume":"2","author":"R Koymans","year":"1990","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255\u2013299 (1990)","journal-title":"Real-Time Syst."},{"issue":"5","key":"25_CR45","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2008","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic, Algebr. Program. 78(5), 293\u2013303 (2008)","journal-title":"J. Logic, Algebr. Program."},{"key":"25_CR46","unstructured":"Lu, H., Forin, A.: The design and implementation of P2V, an architecture for zero-overhead online verification of software programs. Technical Report MSR-TR-2007-99, Microsoft Research, August 2007"},{"key":"25_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-11164-3_24","volume-title":"Runtime Verification","author":"Q Luo","year":"2014","unstructured":"Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: RV-Monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 285\u2013300. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11164-3_24"},{"key":"25_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30206-3_12"},{"key":"25_CR49","doi-asserted-by":"crossref","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., 1\u201341 (2011)","DOI":"10.1007\/s10009-011-0198-6"},{"key":"25_CR50","doi-asserted-by":"crossref","unstructured":"Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: 2015 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 494\u2013503, May 2015","DOI":"10.1109\/IPDPS.2015.95"},{"key":"25_CR51","doi-asserted-by":"crossref","unstructured":"Navabpour, S., Joshi, Y., Wu, C.W.W., Berkovich, S., Medhat, R., Bonakdarpour, B., Fischmeister, S.: RiTHM: a tool for enabling time-triggered runtime verification for c programs. In: ACM Symposium on the Foundations of Software Engineering (FSE), pp. 603\u2013606 (2013)","DOI":"10.1145\/2491411.2494596"},{"issue":"3","key":"25_CR52","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic 5(3), 403\u2013435 (2004)","journal-title":"ACM Trans. Comput. Logic"},{"key":"25_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-75142-7_32","volume-title":"Distributed Computing","author":"VA Ogale","year":"2007","unstructured":"Ogale, V.A., Garg, V.K.: Detecting temporal logic predicates on distributed computations. In: Pelc, A. (ed.) DISC 2007. LNCS, vol. 4731, pp. 420\u2013434. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75142-7_32"},{"key":"25_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-85778-5_1","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"J Ouaknine","year":"2008","unstructured":"Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1\u201313. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-85778-5_1"},{"key":"25_CR55","doi-asserted-by":"crossref","unstructured":"Pastore, F., Mariani, L.: AVA: supporting debugging with failure interpretations. In: Sixth IEEE International Conference on Software Testing, Verification and Validation, ICST 2013, Luxembourg, 18\u201322 March 2013, pp. 416\u2013421 (2013)","DOI":"10.1109\/ICST.2013.58"},{"key":"25_CR56","doi-asserted-by":"crossref","unstructured":"Pellizzoni, R., Meredith, P., Caccamo, M., Rosu, G.: Hardware runtime monitoring for dependable COTS-based real-time embedded systems. In: Real-Time Systems Symposium 2008, pp. 481\u2013491, November 2008","DOI":"10.1109\/RTSS.2008.43"},{"key":"25_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-319-23820-3_20","volume-title":"Runtime Verification","author":"G Reger","year":"2015","unstructured":"Reger, G.: Suggesting edits to explain failing traces. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 287\u2013293. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-23820-3_20"},{"key":"25_CR58","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, Heidelberg (2015). doi: 10.1007\/978-3-319-23820-3_14"},{"key":"25_CR59","unstructured":"Renberg, A.: Test-inspired runtime verification. Master\u2019s thesis, Royal Institute of Technology (KTH), Stockholm (2014)"},{"key":"25_CR60","unstructured":"Russ, A.: Detecting security incidents using windows workstation event logs. Technical report, Sans Institute InfoSec Reading Room (2013)"},{"key":"25_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/11874683_3","volume-title":"Computer Science Logic","author":"L Segoufin","year":"2006","unstructured":"Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41\u201357. Springer, Heidelberg (2006). doi: 10.1007\/11874683_3"},{"key":"25_CR62","doi-asserted-by":"crossref","unstructured":"Selyunin, K., Nguyen, T., Bartocci, E., Nickovic, D., Grosu, R.: Monitoring of MTL specifications with IBM\u2019s spiking-neuron model. In: 2016 Design, Automation Test in Europe Conference Exhibition (DATE), pp. 924\u2013929, March 2016","DOI":"10.3850\/9783981537079_0139"},{"issue":"2","key":"25_CR63","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1016\/S1571-0661(04)81041-7","volume":"89","author":"A Sen","year":"2003","unstructured":"Sen, A., Garg, V.K.: Rv \u20192003, run-time verification (satellite workshop of cav \u201903) partial order trace analyzer (pota) for distributed programs. Electron. Not. Theoret. Comput. Sci. 89(2), 22\u201343 (2003)","journal-title":"Electron. Not. Theoret. Comput. Sci."},{"key":"25_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-27860-3_17","volume-title":"Principles of Distributed Systems","author":"A Sen","year":"2004","unstructured":"Sen, A., Garg, V.K.: Detecting temporal logic predicates in distributed programs using computation slicing. In: Papatriantafilou, M., Hunel, P. (eds.) OPODIS 2003. LNCS, vol. 3144, pp. 171\u2013183. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27860-3_17"},{"key":"25_CR65","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). doi: 10.1007\/978-3-642-35632-2_16"},{"issue":"3","key":"25_CR66","doi-asserted-by":"crossref","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_CR67","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). doi: 10.1007\/978-3-642-29860-8_15"},{"key":"25_CR68","doi-asserted-by":"crossref","first-page":"743","DOI":"10.1093\/logcom\/exn078","volume":"20","author":"V Stolz","year":"2010","unstructured":"Stolz, V.: Temporal assertions with parametrized propositions*. J. Log. Comput. 20, 743\u2013757 (2010)","journal-title":"J. Log. Comput."},{"key":"25_CR69","doi-asserted-by":"crossref","unstructured":"Todman, T., Stilkerich, S., Luk, W.: In-circuit temporal monitors for runtime verification of reconfigurable designs. In: Proceedings of the 52nd Annual Design Automation Conference, DAC 2015, pp. 50:1\u201350:6. ACM, New York (2015)","DOI":"10.1145\/2744769.2744856"},{"issue":"5","key":"25_CR70","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1049\/iet-sen:20060076","volume":"1","author":"C Watterson","year":"2007","unstructured":"Watterson, C., Heffernan, D.: Runtime verification and monitoring of embedded systems. IET Softw. 1(5), 172\u2013179 (2007)","journal-title":"IET Softw."}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,9]],"date-time":"2022-07-09T19:19:00Z","timestamp":1657394340000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}