{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T21:56:02Z","timestamp":1777499762145,"version":"3.51.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031150760","type":"print"},{"value":"9783031150777","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-15077-7_7","type":"book-chapter","created":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T05:02:57Z","timestamp":1661144577000},"page":"114-133","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Bounded-Memory Runtime Enforcement"],"prefix":"10.1007","author":[{"given":"Saumya","family":"Shankar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antoine","family":"Rollet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Srinivas","family":"Pinisetty","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yli\u00e8s","family":"Falcone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,23]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Beauquier, D., Cohen, J., Lanotte, R.: Security policies enforcement using finite and pushdown edit automata. Int. J. Inf. Sec. 12(4), 319\u2013336 (2013). https:\/\/doi.org\/10.1007\/s10207-013-0195-8, http:\/\/dx.doi.org\/10.1007\/s10207-013-0195-8","DOI":"10.1007\/s10207-013-0195-8"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-19125-1_6","volume-title":"Engineering Secure Software and Systems","author":"N Bielova","year":"2011","unstructured":"Bielova, N., Massacci, F.: Predictability of enforcement. In: Erlingsson, \u00da., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 73\u201386. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19125-1_6"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-46681-0_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 533\u2013548. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_51"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Dolzhenko, E., Ligatti, J., Reddy, S.: Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Secur. 14(1), 47\u201360 (2015). https:\/\/doi.org\/10.1007\/s10207-014-0239-8","DOI":"10.1007\/s10207-014-0239-8"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-04694-0_4","volume-title":"Runtime Verification","author":"Y Falcone","year":"2009","unstructured":"Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40\u201359. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04694-0_4"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Fernandez, J., Mounier, L.: What can you verify and enforce at runtime? Int. J. Softw. Tools Technol. Transf. 14(3), 349\u2013382 (2012). https:\/\/doi.org\/10.1007\/s10009-011-0196-8","DOI":"10.1007\/s10009-011-0196-8"},{"key":"7_CR7","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.scico.2016.02.008","volume":"123","author":"Y Falcone","year":"2016","unstructured":"Falcone, Y., J\u00e9ron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Syst. Control Lett. 123, 2\u201341 (2016). https:\/\/doi.org\/10.1016\/j.scico.2016.02.008","journal-title":"Syst. Control Lett."},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-319-75632-5_4","volume-title":"Lectures on Runtime Verification","author":"Y Falcone","year":"2018","unstructured":"Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 103\u2013134. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_4"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Mounier, L., Fernandez, J., Richier, J.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223\u2013262 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0114-4","DOI":"10.1007\/s10703-011-0114-4"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Fong, P.W.L.: Access control by tracking shallow execution history. In: IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004, pp. 43\u201355 (2004). https:\/\/doi.org\/10.1109\/SECPRI.2004.1301314","DOI":"10.1109\/SECPRI.2004.1301314"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Sec. 4(1-2), 2\u201316 (2005). https:\/\/doi.org\/10.1007\/s10207-004-0046-8","DOI":"10.1007\/s10207-004-0046-8"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12(3) (2009). https:\/\/doi.org\/10.1145\/1455526.1455532, https:\/\/doi.org\/10.1007\/s10207-004-0046-8","DOI":"10.1145\/1455526.1455532"},{"issue":"3","key":"7_CR13","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s10703-014-0215-y","volume":"45","author":"S Pinisetty","year":"2014","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Nguena Timo, O.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des. 45(3), 381\u2013422 (2014). https:\/\/doi.org\/10.1007\/s10703-014-0215-y","journal-title":"Formal Methods Syst. Des."},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-35632-2_23","volume-title":"Runtime Verification","author":"S Pinisetty","year":"2013","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Nguena Timo, O.L.: Runtime enforcement of timed properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 229\u2013244. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_23"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Pinisetty, S., Preoteasa, V., Tripakis, S., J\u00e9ron, T., Falcone, Y., Marchand, H.: Predictive runtime enforcement. Formal Methods Syst. Des. 51(1), 154\u2013199 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0271-1","DOI":"10.1007\/s10703-017-0271-1"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Roop, P.S., Smyth, S., Tripakis, S., Hanxleden, R.V.: Runtime enforcement of reactive systems using synchronous enforcers. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, pp. 80\u201389 (2017)","DOI":"10.1145\/3092282.3092291"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Renard, M., Falcone, Y., Rollet, A., J\u00e9ron, T., Marchand, H.: Optimal enforcement of (timed) properties with uncontrollable events. Math. Struct. Comput. Sci. 1\u201346 (2017). https:\/\/doi.org\/10.1017\/S0960129517000123","DOI":"10.1017\/S0960129517000123"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Renard, M., Falcone, Y., Rollet, A., Pinisetty, S., J\u00e9ron, T., Marchand, H.: Enforcement of (timed) properties with uncontrollable events. In: Theoretical Aspects of Computing - ICTAC 2015\u201312th International Colloquium Cali, Colombia, October 29\u201331, 2015, Proceedings, pp. 542\u2013560 (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_31","DOI":"10.1007\/978-3-319-25150-9_31"},{"issue":"2","key":"7_CR19","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/s00165-020-00515-2","volume":"32","author":"M Renard","year":"2020","unstructured":"Renard, M., Rollet, A., Falcone, Y.: Runtime enforcement of timed properties using games. Formal Aspects Comput. 32(2), 315\u2013360 (2020)","journal-title":"Formal Aspects Comput."},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Roc SU, G.: On safety properties and their monitoring. Sci. Ann. Comput. Sci. 22(2), 327\u2013365 (2012). https:\/\/doi.org\/10.7561\/SACS.2012.2.327","DOI":"10.7561\/SACS.2012.2.327"},{"issue":"1","key":"7_CR21","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. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000). https:\/\/doi.org\/10.1145\/353323.353382","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Talhi, C., Tawbi, N., Debbabi, M.: Execution monitoring enforcement under memory-limitation constraints. Inf. Comput. 206(2), 158\u2013184 (2008). https:\/\/doi.org\/10.1016\/j.ic.2007.07.009, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540107001320, joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA 2006)","DOI":"10.1016\/j.ic.2007.07.009"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Wu, M., Zeng, H., Wang, C.: Synthesizing runtime enforcer of safety properties under burst error. In: NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, 7\u20139 June 2016, Proceedings, pp. 65\u201381 (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_6","DOI":"10.1007\/978-3-319-40648-0_6"}],"updated-by":[{"DOI":"10.1007\/978-3-031-15077-7_9","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2022,12,3]],"date-time":"2022-12-03T00:00:00Z","timestamp":1670025600000}}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15077-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,2]],"date-time":"2022-12-02T15:16:07Z","timestamp":1669994167000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15077-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150760","9783031150777"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15077-7_7","relation":{"correction":[{"id-type":"doi","id":"10.1007\/978-3-031-15077-7_9","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"23 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"3 December 2022","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"In the originally published version of chapter 7 \u201cBounded-Memory Runtime Enforcement\u201d the Figure 3 was incorrect. The Figure 3 has now been corrected.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin2022chi.web.illinois.edu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}