{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:52:47Z","timestamp":1743022367469,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030614690"},{"type":"electronic","value":"9783030614706"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-61470-6_6","type":"book-chapter","created":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T18:03:12Z","timestamp":1603735392000},"page":"72-92","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Unifying Framework for Dynamic Monitoring and a Taxonomy of Optimizations"],"prefix":"10.1007","author":[{"given":"Marie-Christine","family":"Jakobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heiko","family":"Mantel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,27]]},"reference":[{"key":"6_CR1","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book - From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"issue":"1","key":"6_CR2","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/s10703-017-0274-y","volume":"51","author":"W Ahrendt","year":"2017","unstructured":"Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools. Formal Methods Syst. Des. 51(1), 200\u2013265 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-34026-0_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"W Ahrendt","year":"2012","unstructured":"Ahrendt, W., Pace, G.J., Schneider, G.: A unified approach for static and runtime verification: framework and applications. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 312\u2013326. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34026-0_24"},{"key":"6_CR4","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21, 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Azzopardi, S., Colombo, C., Pace, G.J.: Control-flow residual analysis for symbolic automata. In: Pre- and Post-Deployment Verification Techniques. EPTCS, vol. 254, pp. 29\u201343 (2017)","DOI":"10.4204\/EPTCS.254.3"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Azzopardi, S., Colombo, C., Pace, G.J.: CLARVA: model-based residual verification of Java programs. In: Model-Driven Engineering and Software Development, pp. 352\u2013359 (2020)","DOI":"10.5220\/0008966603520359"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5","volume-title":"Lectures on Runtime Verification Introductory and Advanced Topics","year":"2018","unstructured":"Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification Introductory and Advanced Topics. LNCS, vol. 10457. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Jug\u00e9, V., Klaedtke, F., Zalinescu, E.: Enforceable security policies revisited. Trans. Inf. Syst. Secur. 16(1), 3:1\u20133:26 (2013)","DOI":"10.1145\/2487222.2487225"},{"key":"6_CR9","doi-asserted-by":"crossref","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., Moss, J.E.B., Phansalkar, A., Stefanovic, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: Object-Oriented Programming, Systems, Languages, and Applications, pp. 169\u2013190 (2006)","DOI":"10.1145\/1167473.1167488"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Bodden, E.: Efficient hybrid typestate analysis by determining continuation-equivalent states. In: International Conference on Software Engineering, pp. 5\u201314 (2010)","DOI":"10.1145\/1806799.1806805"},{"issue":"3","key":"6_CR11","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10009-010-0183-5","volume":"14","author":"E Bodden","year":"2012","unstructured":"Bodden, E., Hendren, L.J.: The Clara framework for hybrid typestate analysis. J. Softw. Tools Technol. Transf. 14(3), 307\u2013326 (2012)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-540-77395-5_3","volume-title":"Runtime Verification","author":"E Bodden","year":"2007","unstructured":"Bodden, E., Hendren, L., Lam, P., Lhot\u00e1k, O., Naeem, N.A.: Collaborative runtime verification with tracematches. In: Sokolsky, O., Ta\u015f\u0131ran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 22\u201337. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77395-5_3"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-03240-0_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"C Colombo","year":"2009","unstructured":"Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 135\u2013149. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03240-0_13"},{"issue":"12","key":"6_CR14","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1109\/TSE.2004.91","volume":"30","author":"N Delgado","year":"2004","unstructured":"Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. Trans. Softw. Eng. 30(12), 859\u2013872 (2004)","journal-title":"Trans. Softw. Eng."},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-38004-4_1","volume-title":"Security and Trust Management","author":"P Dr\u00e1bik","year":"2013","unstructured":"Dr\u00e1bik, P., Martinelli, F., Morisset, C.: Cost-aware runtime enforcement of security policies. In: J\u00f8sang, A., Samarati, P., Petrocchi, M. (eds.) STM 2012. LNCS, vol. 7783, pp. 1\u201316. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38004-4_1"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Diep, M., Elbaum, S.G.: Reducing the cost of path property monitoring through sampling. In: Automated Software Engineering, pp. 228\u2013237 (2008)","DOI":"10.1109\/ASE.2008.33"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Kinneer, A., Elbaum, S.G.: Adaptive online program analysis. In: International Conference on Software Engineering, pp. 220\u2013229 (2007)","DOI":"10.1109\/ICSE.2007.12"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis. In: Automated Software Engineering, pp. 124\u2013133 (2007)","DOI":"10.1145\/1321631.1321651"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Erlingsson, U., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: New Security Paradigms, pp. 87\u201395 (1999)","DOI":"10.1145\/335169.335201"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-030-03769-7_14","volume-title":"Runtime Verification","author":"Y Falcone","year":"2018","unstructured":"Falcone, Y., Krsti\u0107, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 241\u2013262. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_14"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Fei, L., Midkiff, S.P.: Artemis: practical runtime monitoring of applications for execution anomalies. In: Programming Language Design and Implementation, pp. 84\u201395 (2006)","DOI":"10.1145\/1133255.1133992"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-642-31424-7_39","volume-title":"Computer Aided Verification","author":"M Fredrikson","year":"2012","unstructured":"Fredrikson, M., et al.: Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 548\u2013563. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_39"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-13841-1_21","volume-title":"Information Systems Security","author":"R Gay","year":"2014","unstructured":"Gay, R., Hu, J., Mantel, H.: CliSeAu: securing distributed Java programs by cooperative dynamic enforcement. In: Prakash, A., Shyamasundar, R. (eds.) ICISS 2014. LNCS, vol. 8880, pp. 378\u2013398. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13841-1_21"},{"issue":"3","key":"6_CR24","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1145\/243439.243447","volume":"28","author":"ND Jones","year":"1996","unstructured":"Jones, N.D.: An introduction to partial evaluation. ACM Comput. Surv. 28(3), 480\u2013503 (1996)","journal-title":"ACM Comput. Surv."},{"issue":"47\u201349","key":"6_CR25","doi-asserted-by":"publisher","first-page":"5010","DOI":"10.1016\/j.tcs.2009.07.049","volume":"410","author":"J Kao","year":"2009","unstructured":"Kao, J., Rampersad, N., Shallit, J.O.: On NFAs where all states are final, initial, or both. Theoret. Comput. Sci. 410(47\u201349), 5010\u20135021 (2009)","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Automata Studies, pp. 3\u201341 (1956)","DOI":"10.1515\/9781400882618-002"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-29860-8_4","volume-title":"Runtime Verification","author":"M Leucker","year":"2012","unstructured":"Leucker, M.: Teaching runtime verification. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 34\u201348. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_4"},{"issue":"5","key":"6_CR28","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. Logic Algebraic Program. 78(5), 293\u2013303 (2009)","journal-title":"J. Logic Algebraic Program."},{"issue":"1\u20132","key":"6_CR29","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. J. Inf. Secur. 4(1\u20132), 2\u201316 (2005)","journal-title":"J. Inf. Secur."},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Purandare, R., Dwyer, M.B., Elbaum, S.G.: Monitor optimization via stutter-equivalent loop transformation. In: Object-Oriented Programming, Systems, Languages, and Applications, pp. 270\u2013285 (2010)","DOI":"10.1145\/1932682.1869483"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Purandare, R., Dwyer, M.B., Elbaum, S.G.: Optimizing monitoring of finite state properties through monitor compaction. In: Software Testing and Analysis, pp. 280\u2013290 (2013)","DOI":"10.1145\/2483760.2483762"},{"key":"6_CR32","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/j.jss.2016.12.034","volume":"125","author":"R Rabiser","year":"2017","unstructured":"Rabiser, R., Guinea, S., Vierhauser, M., Baresi, L., Gr\u00fcnbacher, P.: A comparison framework for runtime monitoring approaches. J. Syst. Softw. 125, 309\u2013321 (2017)","journal-title":"J. Syst. Softw."},{"issue":"1","key":"6_CR33","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"Trans. Inf. Syst. Secur."},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-642-40787-1_16","volume-title":"Runtime Verification","author":"C Wang","year":"2013","unstructured":"Wang, C., Chen, Z., Mao, X.: Optimizing nop-shadows typestate analysis by filtering interferential configurations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 269\u2013284. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_16"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-40561-7_17","volume-title":"Software Engineering and Formal Methods","author":"D Wonisch","year":"2013","unstructured":"Wonisch, D., Schremmer, A., Wehrheim, H.: Zero overhead runtime monitoring. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 244\u2013258. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40561-7_17"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-40787-1_18","volume-title":"Runtime Verification","author":"CWW Wu","year":"2013","unstructured":"Wu, C.W.W., Kumar, D., Bonakdarpour, B., Fischmeister, S.: Reducing monitoring overhead by integrating event- and time-triggered techniques. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 304\u2013321. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_18"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-46982-9_24","volume-title":"Runtime Verification","author":"Y Yamagata","year":"2016","unstructured":"Yamagata, Y., et al.: Runtime monitoring for concurrent systems. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 386\u2013403. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_24"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61470-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,10]],"date-time":"2023-10-10T16:44:35Z","timestamp":1696956275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61470-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030614690","9783030614706"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61470-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"27 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}