{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T04:57:25Z","timestamp":1764133045578,"version":"3.41.0"},"reference-count":85,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,4,7]],"date-time":"2017-04-07T00:00:00Z","timestamp":1491523200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s10009-017-0454-5","type":"journal-article","created":{"date-parts":[[2017,4,7]],"date-time":"2017-04-07T07:26:06Z","timestamp":1491549966000},"page":"31-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":48,"title":["First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014"],"prefix":"10.1007","volume":"21","author":[{"given":"Ezio","family":"Bartocci","sequence":"first","affiliation":[]},{"given":"Yli\u00e8s","family":"Falcone","sequence":"additional","affiliation":[]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Colombo","sequence":"additional","affiliation":[]},{"given":"Normann","family":"Decker","sequence":"additional","affiliation":[]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[]},{"given":"Yogi","family":"Joshi","sequence":"additional","affiliation":[]},{"given":"Felix","family":"Klaedtke","sequence":"additional","affiliation":[]},{"given":"Reed","family":"Milewicz","sequence":"additional","affiliation":[]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Rosu","sequence":"additional","affiliation":[]},{"given":"Julien","family":"Signoles","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Thoma","sequence":"additional","affiliation":[]},{"given":"Eugen","family":"Zalinescu","sequence":"additional","affiliation":[]},{"given":"Yi","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,4,7]]},"reference":[{"key":"454_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Rustan, K., Leino, M. (eds.): Proceedings of TACAS 2011: The 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Volume 6605 of LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-19835-9"},{"key":"454_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Deters, M., de Moura, L., Oliveras, Ade, Stump, A.: 6 years of SMT-COMP. J. Autom. Reason. 50(3), 243\u2013277 (2013)","DOI":"10.1007\/s10817-012-9246-5"},{"key":"454_CR3","doi-asserted-by":"crossref","unstructured":"Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.E.: Quantified event automata: towards expressive and efficient runtime monitors. In: Proceedings of FM 2012: The 18th International Symposium on Formal Methods, Volume 7436 of LNCS, pp. 68\u201384. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-32759-9_9"},{"key":"454_CR4","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour and Smolka [24], pp. 1\u20139","DOI":"10.1007\/978-3-319-11164-3_1"},{"key":"454_CR5","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Proceedings of CMSB 2013: The 11th International Conference on Computational Methods in Systems Biology, Volume 8130 of LNCS, pp. 164\u2013177. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40708-6_13"},{"key":"454_CR6","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Bortolussi, L., Sanguinetti, G.: Data-driven statistical learning of temporal logic properties. In: Proceedings of FORMATS 2014: The 12th International Conference on Formal Modeling and Analysis of Timed Systems, Volume 8711 of LNCS, pp. 23\u201337 (2014)","DOI":"10.1007\/978-3-319-10512-3_3"},{"key":"454_CR7","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y.: Runtime verification and enforcement, the (industrial) application perspective (track introduction). In: Proceedings of ISoLA 2016: The 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, Part II, Volume 9953 of LNCS, pp. 333\u2013338 (2016)","DOI":"10.1007\/978-3-319-47169-3_24"},{"key":"454_CR8","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Proceedings of RV 2012: The 3rd International Conference on Runtime Verification, Volume 7687 of LNCS, pp. 168\u2013182. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-35632-2_18"},{"key":"454_CR9","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Li\u00f2, P.: Computational modeling, formal analysis, and tools for systems biology. PLoS Comput. Biol. 12(1), e1004591 (2016)","DOI":"10.1371\/journal.pcbi.1004591"},{"key":"454_CR10","doi-asserted-by":"crossref","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Z\u0103linescu, E.: MONPOLY: Monitoring usage-control policies. In: Proceedings of RV 2011: The 2nd International Conference on Runtime Verification, Volume 7186 of LNCS, pp. 360\u2013364. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-29860-8_27"},{"issue":"10","key":"454_CR11","doi-asserted-by":"publisher","first-page":"1403","DOI":"10.1109\/TSE.2013.18","volume":"39","author":"D Basin","year":"2013","unstructured":"Basin, D., Harvan, M., Klaedtke, F., Z\u0103linescu, E.: Monitoring data usage in distributed systems. IEEE Trans. Softw. Eng. 39(10), 1403\u20131426 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"454_CR12","doi-asserted-by":"crossref","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)","DOI":"10.1145\/2699444"},{"issue":"2","key":"454_CR13","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1016\/j.ipl.2014.09.009","volume":"115","author":"D Basin","year":"2015","unstructured":"Basin, D., Klaedtke, F., Z\u0103linescu, E.: Greedily computing associative aggregations on sliding windows. Inf. Process. Lett. 115(2), 186\u2013192 (2015)","journal-title":"Inf. Process. Lett."},{"issue":"1\u20132","key":"454_CR14","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/s10703-016-0242-y","volume":"49","author":"DA Basin","year":"2016","unstructured":"Basin, D.A., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., Mantel, H.: Scalable offline monitoring. Form. Methods Syst. Des. 49(1\u20132), 75\u2013108 (2016)","journal-title":"Form. Methods Syst. Des."},{"issue":"3","key":"454_CR15","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-015-0222-7","volume":"46","author":"DA Basin","year":"2015","unstructured":"Basin, D.A., Klaedtke, F., Marinovic, S., Z\u0103linescu, E.: Monitoring of temporal first-order properties with aggregations. Form. Methods Syst. Des. 46(3), 262\u2013285 (2015)","journal-title":"Form. Methods Syst. Des."},{"key":"454_CR16","unstructured":"Baudin, P., Filli $$\\hat{a}$$ a ^ tre, J.-C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C Specification Language. Version 1.8, March 2014"},{"key":"454_CR17","unstructured":"Benameur, A., Evans, N.S., Elder, M.C.: MINESTRONE: testing the SOUP. In: Kanich, C., Sherr, M. (eds.) In: 6th Workshop on Cyber Security Experimentation and Test, CSET \u201913, Washington, DC, USA, August 12, 2013. USENIX Association (2013)"},{"key":"454_CR18","unstructured":"Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: 27th IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2013, Cambridge, MA, USA, May 20\u201324, 2013, pp. 1025\u20131036 (2013)"},{"key":"454_CR19","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Competition on software verification\u2014(SV-COMP). In: Proceedings of TACAS 2012: The 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems\u201418th International Conference, Volume 7214 of LNCS, pp. 504\u2013524. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28756-5_38"},{"key":"454_CR20","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Status report on software verification\u2014(competition summary SV-COMP 2014). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings, Volume 8413 of Lecture Notes in Computer Science, pp. 373\u2013388. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"454_CR21","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Software verification and verifiable witnesses\u2014(report on SV-COMP 2015). In: Proceedings of TACAS 2015: The 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, vol. 9035, pp. 401\u2013416. Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"454_CR22","unstructured":"Blackburn, S.M., Garner, R., Hoffmann, C., Khan, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A.L., Jump, M., Lee, H.B., Eliot, J., Moss, B., Phansalkar, A., Stefanovic, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: Tarr, P.L., Cook, W.R. (eds.) Proceedings of the 21th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2006, October 22\u201326, 2006, Portland, Oregon, USA, pp. 169\u2013190. ACM (2006)"},{"issue":"10","key":"454_CR23","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1109\/MC.2012.345","volume":"45","author":"T Boland","year":"2012","unstructured":"Boland, T., Black, P.E.: Juliet 1.1 C\/C++ and Java test suite. Computer 45(10), 88\u201390 (2012)","journal-title":"Computer"},{"key":"454_CR24","doi-asserted-by":"crossref","unstructured":"Bonakdarpour, B., Smolka, S.A. (eds.): Runtime Verification\u20145th International Conference, RV 2014, Toronto, ON, Canada, September 22\u201325, 2014. Proceedings, Volume 8734 of Lecture Notes in Computer Science. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-11164-3"},{"key":"454_CR25","doi-asserted-by":"crossref","unstructured":"Boul\u00e9, M., Zilic, Z.: Incorporating efficient assertion checkers into hardware emulation. In: Proceedings of ICCD, pp. 221\u2013228. IEEE Computer Society Press (2005)","DOI":"10.1109\/ICCD.2005.66"},{"key":"454_CR26","doi-asserted-by":"crossref","unstructured":"Boul\u00e9, M., Zilic, Z.: Efficient automata-based assertion-checker synthesis of PSL properties. In: Proceedings of HLDVT, pp. 69\u201376. IEEE (2006)","DOI":"10.1109\/HLDVT.2006.319966"},{"key":"454_CR27","doi-asserted-by":"crossref","unstructured":"Boul\u00e9, M., Zilic, Z.: Automata-based assertion-checker synthesis of PSL properties. ACM Trans. Des. Autom. Electron. Syst. 13(1), 4:1\u20134:21","DOI":"10.1145\/1297666.1297670"},{"key":"454_CR28","doi-asserted-by":"crossref","unstructured":"Bufo, S., Bartocci, E., Sanguinetti, G., Borelli, M., Lucangelo, U., Bortolussi, L.: Temporal logic based monitoring of assisted ventilation in intensive care patients. In: Steffen, B., Margaria, T. (eds.) Proceedings of ISoLA 2014: 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Volume 8803 of LNCS, pp. 391\u2013403 (2014)","DOI":"10.1007\/978-3-662-45231-8_30"},{"issue":"5","key":"454_CR29","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z Chaochen","year":"1991","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."},{"key":"454_CR30","doi-asserted-by":"crossref","unstructured":"Chen, F., Meredith, P., Jin, D., Rosu, G.: Efficient formalism-independent monitoring of parametric properties. In: IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201909), pp. 383\u2013394 (2009)","DOI":"10.1109\/ASE.2009.50"},{"issue":"3","key":"454_CR31","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/s10703-012-0142-8","volume":"41","author":"C Colombo","year":"2012","unstructured":"Colombo, C., Pace, G., Abela, P.: Safer asynchronous runtime monitoring using compensations. Form. Methods Syst. Des. 41(3), 269\u2013294 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"454_CR32","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J.: Fast-forward runtime monitoring\u2014an industrial case study. In: Runtime Verification, Third International Conference, RV 2012, Volume 7687 of Lecture Notes in Computer Science, pp. 214\u2013228. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-35632-2_22"},{"key":"454_CR33","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Formal Methods for Industrial Critical Systems (FMICS), Volume 5596 of Lecture Notes in Computer Science, pp. 135\u2013149. Springer, Berlin (2008)","DOI":"10.1007\/978-3-642-03240-0_13"},{"key":"454_CR34","doi-asserted-by":"crossref","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Larva\u2014safer monitoring of real-time java programs (tool paper). In: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM \u201909, pp. 33\u201337. IEEE Computer Society, Washington, DC (2009)","DOI":"10.1109\/SEFM.2009.13"},{"key":"454_CR35","doi-asserted-by":"crossref","unstructured":"Dahan, A., Geist, D., Gluhovsky, L., Pidan, D., Shapir, G., Wolfsthal, Y., Benalycherif, L., Kamidem, R., Lahbib, Y.: Combining system level modeling with assertion based verification. In: Proceedings of ISQED 2005: Sixth International Symposium on Quality of Electronic Design, pp. 310\u2013315. IEEE (2005)","DOI":"10.1109\/ISQED.2005.32"},{"key":"454_CR36","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: Proceedings of TIME 2005: The 12th International Symposium on Temporal Representation and Reasoning, pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"key":"454_CR37","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, Nikolaj.: Z3: an efficient SMT solver. In: Ramakrishnan,C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings, Volume 4963 of Lecture Notes in Computer Science, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"454_CR38","doi-asserted-by":"crossref","unstructured":"Decker, N., Leucker, M., Thoma, D.: jUnitRV\u2014adding runtime verification to jUnit. In Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods, 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14\u201316, 2013. Proceedings, Volume 7871 of Lecture Notes in Computer Science, pp. 459\u2013464. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38088-4_34"},{"key":"454_CR39","doi-asserted-by":"crossref","unstructured":"Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings, Volume 8413 of Lecture Notes in Computer Science, pp. 341\u2013356. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54862-8_23"},{"key":"454_CR40","unstructured":"Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18(2), 205\u2013225 (2016)"},{"key":"454_CR41","doi-asserted-by":"crossref","unstructured":"Delahaye, M., Kosmatov, N., Signoles, J.: Common specification language for static and dynamic analysis of C programs. In: Proceedings of SAC \u201913: The 28th Annual ACM Symposium on Applied Computing, pp. 1230\u20131235. ACM (2013)","DOI":"10.1145\/2480362.2480593"},{"key":"454_CR42","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.A.: On Temporal Logic and Signal Processing. In: Chakraborty, S., Mukund, M. (eds.) Proceedings of ATVA 2012: 10th International Symposium on Automated Technology for Verification and Analysis, Thiruvananthapuram, India, October 3\u20136, Volume 7561 of Lecture Notes in Computer Science, pp. 92\u2013106. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-33386-6_9"},{"key":"454_CR43","doi-asserted-by":"crossref","unstructured":"Drago, I., Mellia, M., Munaf\u00f2, M.M., Sperotto, A., Sadre, R., Pras, A.: Inside Dropbox: Understanding personal cloud storage services. In: Proceedings of the 12th ACM SIGCOMM Conference on Internet Measurement, IMC\u201912, pp. 481\u2013494 (2012)","DOI":"10.1145\/2398776.2398827"},{"key":"454_CR44","doi-asserted-by":"crossref","unstructured":"Falcone, Y.: You should better enforce than verify. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G.J., Rosu, G., Sokolsky, O., Tillmann, N. (eds.) Proceedings of the 1st International Conference on Runtime Verification (RV 2010), Volume 6418 of Lecture Notes in Computer Science, pp. 89\u2013105. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16612-9_9"},{"key":"454_CR45","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: 9th International Workshop on Runtime Verification. Selected Papers, vol. 5779, pp. 40\u201359 (2009)","DOI":"10.1007\/978-3-642-04694-0_4"},{"key":"454_CR46","first-page":"141","volume-title":"Engineering Dependable Software Systems, Volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security","author":"Y Falcone","year":"2013","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D., Kalus, G. (eds.) Engineering Dependable Software Systems, Volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security, pp. 141\u2013175. IOS Press, Amsterdam (2013)"},{"key":"454_CR47","unstructured":"Falcone, Y., Nickovic, D., Reger, G., Thoma, D.: Second international competition on runtime verification\u2014crv 15. In: Runtime Verification\u201415th International Conference, RV 2015, Vienna, Austria, 2015. Proceedings, vol. 9333, pp. 365\u2013382 (2015)"},{"key":"454_CR48","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Kuhtz, L.: Monitor circuits for ltl with bounded and unbounded future. In: Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Volume 5779 of LNCS, pp. 60\u201375 (2009)","DOI":"10.1007\/978-3-642-04694-0_5"},{"issue":"3","key":"454_CR49","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1145\/5666.5673","volume":"29","author":"PJ Fleming","year":"1986","unstructured":"Fleming, P.J., Wallace, J.J.: How not to lie with statistics: the correct way to summarize benchmark results. Commun. ACM 29(3), 218\u2013221 (1986)","journal-title":"Commun. ACM"},{"key":"454_CR50","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, CDC 2014, Los Angeles, CA, USA, December 15\u201317, 2014, pp. 108\u2013113. IEEE (2014)"},{"key":"454_CR51","unstructured":"Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) Verified Software: Theories, Tools, Experiments, First IFIP TC 2\/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10\u201313, 2005, Revised Selected Papers and Discussions, Volume 4171 of Lecture Notes in Computer Science, pp. 374\u2013383. Springer, Berlin (2005)"},{"key":"454_CR52","doi-asserted-by":"crossref","unstructured":"Havelund, K., Reger, G.: Specification of parametric monitors\u2014quantified event automata versus rule systems. In: Drechsler, R., K\u00fchne, U. (eds.) Formal Modeling and Verification of Cyber-Physical Systems. Springer, Fachmedien Wiesbaden (2015)","DOI":"10.1007\/978-3-658-09994-7_6"},{"key":"454_CR53","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change\u20145th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, October 15\u201318, 2012, Proceedings, Part I, Volume 7609 of Lecture Notes in Computer Science, pp. 608\u2013614. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-34026-0_45"},{"issue":"5","key":"454_CR54","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/s10009-014-0337-y","volume":"16","author":"F Howar","year":"2014","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems\u2014the RERS challenges 2012 and 2013. STTT 16(5), 457\u2013464 (2014)","journal-title":"STTT"},{"issue":"6","key":"454_CR55","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-015-0396-8","volume":"17","author":"M Huisman","year":"2015","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: Verifythis 2012\u2014a program verification competition. STTT 17(6), 647\u2013657 (2015)","journal-title":"STTT"},{"key":"454_CR56","unstructured":"Jakobsson, A., Kosmatov, N., Signoles, J.: Fast as a shadow, expressive as a tree: hybrid memory monitoring for C. In: Wainwright, R.L., Corchado, J.M., Bechini, A., Hong, J. (eds.) Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, April 13\u201317, 2015, pp. 1765\u20131772. ACM (2015)"},{"key":"454_CR57","doi-asserted-by":"crossref","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ni\u010dkovi\u0107, D.: From signal temporal logic to FPGA monitors. In: Proceedings of MEMOCODE 2015: The ACM\/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218\u2013227. IEEE (2015)","DOI":"10.1109\/MEMCOD.2015.7340489"},{"key":"454_CR58","doi-asserted-by":"crossref","unstructured":"Jaksic, S., Bartocci, E., Grosu, R., Ni\u010dkovi\u0107, D.: Quantitative monitoring of STL with edit distance. In Proceedings of RV 2016: The 7th International Conference on Runtime Verification, LNCS, page to appear (2016)","DOI":"10.1007\/978-3-319-46982-9_13"},{"issue":"1","key":"454_CR59","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1609\/aimag.v33i1.2395","volume":"33","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Mag. 33(1), 89\u201394 (2012)","journal-title":"AI Mag."},{"key":"454_CR60","doi-asserted-by":"crossref","unstructured":"Jin, D., Meredith, P.O., Lee, C., Ro\u015fu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: Proceedings of ICSE 2012: The 34th International Conference on Software Engineering, Zurich, Switzerland, June 2\u20139, pp. 1427\u20131430. IEEE Press (2012)","DOI":"10.1109\/ICSE.2012.6227231"},{"key":"454_CR61","doi-asserted-by":"crossref","unstructured":"Jin, D., Meredith, P.O.N, Griffith, D., Ro\u015fu, G.: Garbage collection for monitoring parametric properties. In: Programming Language Design and Implementation (PLDI\u201911), pp. 415\u2013424. ACM (2011)","DOI":"10.1145\/1993498.1993547"},{"key":"454_CR62","doi-asserted-by":"crossref","unstructured":"Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S., Grosu, G.: Runtime verification with particle filtering. In: Proceedings of RV 2013, The fourth International Conference on Runtime Verification, INRIA Rennes, France, 24\u201327 September, 2013, Volume 8174 of Lecture Notes in Computer Science, pp. 149\u2013166. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40787-1_9"},{"key":"454_CR63","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Form. Asp. Comput. 27(3), 573\u2013609 (2015)"},{"key":"454_CR64","doi-asserted-by":"crossref","unstructured":"Kosmatov, N., Petiot, G., Signoles, J.: An optimized memory monitoring for runtime assertion checking of C programs. In: International Conference on Runtime Verification (RV\u201913), Volume 8174 of LNCS, pp. 167\u2013182. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40787-1_10"},{"issue":"6","key":"454_CR65","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1016\/j.pmcj.2013.07.014","volume":"9","author":"JL Laurila","year":"2013","unstructured":"Laurila, J.L., Gatica-Perez, D., Aad, I., Blom, J., Bornet, O., Do, T.M.T., Dousse, O., Eberle, J., Miettinen, M.: From big smartphone data to worldwide research: the mobile data challenge. Pervasive Mob. Comput. 9(6), 752\u2013771 (2013)","journal-title":"Pervasive Mob. Comput."},{"issue":"5","key":"454_CR66","doi-asserted-by":"publisher","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":"454_CR67","doi-asserted-by":"crossref","unstructured":"Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P.O.N, Serbanuta, T.-F., Rosu, G.: Rv-monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour and Smolka [24], pp. 285\u2013300 (2014)","DOI":"10.1007\/978-3-319-11164-3_24"},{"key":"454_CR68","unstructured":"Medhat, R., Joshi, Y., Bonakdarpour, B., Fischmeister, S.: Accelerated runtime verification of LTL specifications with counting semantics. CoRR abs\/1411.2239 (2014)"},{"issue":"3","key":"454_CR69","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PON Meredith","year":"2012","unstructured":"Meredith, P.O.N., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249\u2013289 (2012)","journal-title":"STTT"},{"key":"454_CR70","doi-asserted-by":"crossref","unstructured":"Milewicz, R., Vanka, R., Tuck, J., Quinlan, D., Pirkelbauer, P.: Runtime checking c programs. In: Proceedings of the 30th Annual ACM Symposium on Applied Computing, pp. 2107\u20132114. ACM (2015)","DOI":"10.1145\/2695664.2695906"},{"key":"454_CR71","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"},{"key":"454_CR72","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Bartocci, E., Ni\u010dkovi\u0107, D., Grosu, R., Jaksic, S., Selyunin, K.: The HARMONIA project: hardware monitoring for automotive systems-of-systems. In: Steffen, B., Margaria, T. (eds.) Proceedings of ISoLA 2016: 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Volume 9953 of LNCS, pp. 371\u2013379. Springer, Berlin (2016)","DOI":"10.1007\/978-3-319-47169-3_28"},{"key":"454_CR73","doi-asserted-by":"crossref","unstructured":"Oliveira, A., Petkovich, J.-C., Reidemeister, T., Fischmeister, S.: DataMill: Rigorous performance evaluation made easy. In: Proceedings of ICPE 2013: The 4th ACM\/SPEC International Conference on Performance Engineering, pp. 137\u2013149. ACM (2013)","DOI":"10.1145\/2479871.2479892"},{"key":"454_CR74","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21\u201327, 2006, Proceedings, Volume 4085 of Lecture Notes in Computer Science, pp. 573\u2013586. Springer, Berlin (2006)","DOI":"10.1007\/11813040_38"},{"key":"454_CR75","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\u201915) (2015)","DOI":"10.1007\/978-3-662-46681-0_55"},{"issue":"3","key":"454_CR76","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/s10703-013-0199-z","volume":"44","author":"T Reinbacher","year":"2014","unstructured":"Reinbacher, T., F\u00fcgger, M., Brauer, J.: Runtime verification of embedded real-time systems. Form. Methods Syst. Des. 44(3), 230\u2013239 (2014)","journal-title":"Form. Methods Syst. Des."},{"key":"454_CR77","doi-asserted-by":"crossref","unstructured":"Reinbacher, T., Rozier, K.Y., Schuman, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings of TACAS 2014, Volume 8413 of LNCS, pp. 357\u2013372. Springer, Berlin (2014)","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"454_CR78","doi-asserted-by":"crossref","unstructured":"Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. STTT 16(5), 493\u2013505 (2014)","DOI":"10.1007\/s10009-014-0338-x"},{"key":"454_CR79","doi-asserted-by":"crossref","unstructured":"Selyunin, K., Nguyen, T., Bartocci, E., Ni\u010dkovi\u0107, D., Grosu, R.: Monitoring of MTL specifications With IBM\u2019s spiking-neuron model. In: Proceedings of DATE 2016: The 19th Design, Automation and Test in Europe Conference and Exhibition, pp. 924\u2013929. IEEE (2016)","DOI":"10.3850\/9783981537079_0139"},{"key":"454_CR80","unstructured":"Signoles, J.: E-ACSL: Executable ANSI\/ISO C Specification Language, Version 1.5-4, March 2014. http:\/\/frama-c.com\/download\/e-acsl\/e-acsl.pdf"},{"key":"454_CR81","unstructured":"Signoles, J.: E-ACSL User Manual, March 2014. http:\/\/frama-c.com\/download\/e-acsl\/e-acsl-manual.pdf"},{"issue":"3","key":"454_CR82","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10009-011-0218-6","volume":"14","author":"O Sokolsky","year":"2012","unstructured":"Sokolsky, O., Havelund, K., Lee, I.: Introduction to the special section on runtime verification. STTT 14(3), 243\u2013247 (2012)","journal-title":"STTT"},{"key":"454_CR83","doi-asserted-by":"crossref","unstructured":"Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Proceedings of RV 2011. The Second International Conference on Runtime verification, San Francisco, CA, USA, Volume 7186 of Lecture Notes in Computer Science, pp. 193\u2013207. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-29860-8_15"},{"issue":"1","key":"454_CR84","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/AIC-2010-0483","volume":"24","author":"G Sutcliffe","year":"2011","unstructured":"Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition\u2014CASC-J5. AI Commun. 24(1), 75\u201389 (2011)","journal-title":"AI Commun."},{"issue":"4","key":"454_CR85","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1016\/j.comnet.2008.09.022","volume":"53","author":"M Zink","year":"2009","unstructured":"Zink, M., Kyoungwon, S., Gu, Y., Kurose, J.: Characteristics of youtube network traffic at a campus network\u2014measurements, models, and implications. Comput. Netw. 53(4), 501\u2013514 (2009)","journal-title":"Comput. Netw."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0454-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0454-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0454-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:18:40Z","timestamp":1750195120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0454-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,7]]},"references-count":85,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["454"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0454-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2017,4,7]]},"assertion":[{"value":"7 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}