{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T20:05:35Z","timestamp":1760731535085,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031124402"},{"type":"electronic","value":"9783031124419"}],"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-12441-9_11","type":"book-chapter","created":{"date-parts":[[2022,7,29]],"date-time":"2022-07-29T10:23:34Z","timestamp":1659090214000},"page":"212-229","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Automating Safety Proofs About Cyber-Physical Systems Using Rewriting Modulo SMT"],"prefix":"10.1007","author":[{"given":"Vivek","family":"Nigam","sequence":"first","affiliation":[]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,30]]},"reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Robot. 30(4), 903\u2013918 (2014)","journal-title":"IEEE Trans. Robot."},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.scico.2019.03.006","volume":"178","author":"K Bae","year":"2019","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20\u201342 (2019)","journal-title":"Sci. Comput. Program."},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol. 13243. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Dantas, Y.G., Nigam, V., Talcott, C.L.: A formal security assessment framework for cooperative adaptive cruise control. In: IEEE Vehicular Networking Conference, VNC 2020, New York, NY, USA, pp. 16\u201318 December 2020, pp. 1\u20138. IEEE (2020)","DOI":"10.1109\/VNC51378.2020.9318334"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Desai, A., Ghosh, S., Seshia, S.A., Shankar, N., Tiwari, A.: SOTER: a runtime assurance framework for programming safe robotics systems. In: 49th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, DSN 2019, Portland, OR, USA, 24\u201327 June 2019, pp. 138\u2013150. IEEE (2019)","DOI":"10.1109\/DSN.2019.00027"},{"key":"11_CR8","unstructured":"Dosovitskiy, A., Ros, G., Codevilla, F., L\u00f3pez, A.M., Koltun, V.: CARLA: an open urban driving simulator. In: 1st Annual Conference on Robot Learning, CoRL 2017, Mountain View, California, USA, 13\u201315 November 2017, Proceedings, vol. 78 of Proceedings of Machine Learning Research, pp. 1\u201316. PMLR (2017)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22\u201326 June 2019, pp. 63\u201378. ACM (2019)","DOI":"10.1145\/3314221.3314633"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-319-74781-1_28","volume-title":"Software Engineering and Formal Methods","author":"IA Mason","year":"2018","unstructured":"Mason, I.A., Nigam, V., Talcott, C., Brito, A.: A framework for analyzing adaptive autonomous aerial vehicles. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 406\u2013422. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-74781-1_28"},{"key":"11_CR11","unstructured":"SAE J3016. https:\/\/www.sae.org\/news\/2019\/01\/sae-updates-j3016-automated-driving-graphic (2021)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-030-54549-9_15","volume-title":"Computer Safety, Reliability, and Security","author":"S Jha","year":"2020","unstructured":"Jha, S., Rushby, J., Shankar, N.: Model-centered assurance for autonomous systems. In: Casimiro, A., Ortmeier, F., Bitsch, F., Ferreira, P. (eds.) SAFECOMP 2020. LNCS, vol. 12234, pp. 228\u2013243. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54549-9_15"},{"key":"11_CR13","unstructured":"Kalra, N., Paddock, S.M.: Driving to safety. https:\/\/www.rand.org\/content\/dam\/rand\/pubs\/research_reports\/RR1400\/RR1478\/RAND_RR1478.pdf (2021)"},{"key":"11_CR14","unstructured":"MaudeSE. https:\/\/github.com\/maude-se\/maude-se.github.io (2021)"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Menzel, T., Bagschik, G., Maurer, M.: Scenarios for development, test and validation of automated vehicles. In: 2018 IEEE Intelligent Vehicles Symposium, IV 2018, Changshu, Suzhou, China, 26\u201330 June 2018, pp. 1821\u20131827. IEEE (2018)","DOI":"10.1109\/IVS.2018.8500406"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-030-58298-2_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"F Moradi","year":"2020","unstructured":"Moradi, F., Asadollah, S.A., Sedaghatbaf, A., Causevic, A., Sirjani, M., Talcott, C.L.: An actor-based approach for security analysis of cyber-physical systems. In: ter Beek, M.H., Nickovic, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 130\u2013147. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_5"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Abstraction and completeness for real-time maude. In: Denker, G., Talcott, C.L. (eds.) Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, 1\u20132 April 2006, vol. 174 of Electronic Notes in Theoretical Computer Science, pp. 5\u201327. Elsevier (2006)","DOI":"10.1016\/j.entcs.2007.06.005"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-78800-3_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PC \u00d6lveczky","year":"2008","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: The real-time maude tool. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 332\u2013336. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_23"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"87456","DOI":"10.1109\/ACCESS.2020.2993730","volume":"8","author":"S Riedmaier","year":"2020","unstructured":"Riedmaier, S., Ponn, T., Ludwig, D., Schick, B., Diermeyer, F.: Survey on scenario-based safety assessment of automated vehicles. IEEE Access 8, 87456\u201387477 (2020)","journal-title":"IEEE Access"},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Logical Algebraic Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Rubio, R.: Maude as a library: an efficient all-purpose programming interface. In: Rewriting Logic and its Applications (WRLA) (2022)","DOI":"10.1007\/978-3-031-12441-9_14"},{"key":"11_CR22","unstructured":"Shalev-Shwartz, S., Shammah, S., Shashua, A.: On a formal model of safe and scalable self-driving cars. CoRR, abs\/1708.06374 (2017)"},{"key":"11_CR23","unstructured":"Sifakis, J.: Autonomous systems - an architectural characterization. CoRR, abs\/1811.10277 (2018)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-34096-8_1","volume-title":"Formal Methods for the Quantitative Evaluation of Collective Adaptive Systems","author":"C Talcott","year":"2016","unstructured":"Talcott, C., Nigam, V., Arbab, F., Kapp\u00e9, T.: Formal specification and analysis of robust adaptive distributed cyber-physical systems. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 1\u201335. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-34096-8_1"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-15545-6_18","volume-title":"Software, Services, and Systems","author":"C Talcott","year":"2015","unstructured":"Talcott, C., Arbab, F., Yadav, M.: Soft agents: exploring soft constraints to model robust adaptive distributed cyber-physical agent systems. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 273\u2013290. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15545-6_18"},{"issue":"1","key":"11_CR26","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1109\/TITS.2017.2700021","volume":"19","author":"S van de Hoef","year":"2018","unstructured":"van de Hoef, S., Johansson, K.H., Dimarogonas, D.V.: Fuel-efficient en route formation of truck platoons. IEEE Trans. Intell. Transp. Syst. 19(1), 102\u2013112 (2018)","journal-title":"IEEE Trans. Intell. Transp. Syst."}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-12441-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,12]],"date-time":"2023-02-12T23:34:09Z","timestamp":1676244849000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-12441-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031124402","9783031124419"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-12441-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WRLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Rewriting Logic and its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wrla2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sv.postech.ac.kr\/wrla2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}