{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,4]],"date-time":"2026-07-04T05:06:03Z","timestamp":1783141563287,"version":"3.54.6"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031606977","type":"print"},{"value":"9783031606984","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_19","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"322-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Formal Verification Framework for\u00a0Runtime Assurance"],"prefix":"10.1007","author":[{"given":"J. Tanner","family":"Slagel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lauren M.","family":"White","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Dutle","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar A.","family":"Mu\u00f1oz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Crespo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"ASTM International: Standard practice for methods to safely bound behavior of aircraft systems containing complex functions using run-time assurance, ASTM F3269-21 (2021). https:\/\/doi.org\/10.1520\/F3269-21","DOI":"10.1520\/F3269-21"},{"key":"19_CR2","unstructured":"Brat, G., Pai, G.: Runtime assurance of aeronautical products: preliminary recommendations. Technical Memorandum (2023). https:\/\/ntrs.nasa.gov\/citations\/20220015734"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-319-47166-2_31","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"A Goodloe","year":"2016","unstructured":"Goodloe, A.: Challenges in high-assurance runtime verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 446\u2013460. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_31"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10722468_15","volume-title":"SPIN Model Checking and Software Verification","author":"K Havelund","year":"2000","unstructured":"Havelund, K.: Using runtime analysis to guide model checking of java programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 245\u2013264. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722468_15"},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"Jeannin, J., et al.: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. Int. J. Softw. Tools Technol. Transf. 19(6) (2017). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_2","DOI":"10.1007\/978-3-662-46681-0_2"},{"key":"19_CR6","doi-asserted-by":"publisher","unstructured":"Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: Formally specified monitoring of temporal properties. In: Euromicro Conference on Real-Time Systems. Euromicro RTS. IEEE (1999). https:\/\/doi.org\/10.1109\/EMRTS.1999.777457","DOI":"10.1109\/EMRTS.1999.777457"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"19_CR8","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2) (2008). https:\/\/doi.org\/10.1007\/s10817-008-9103-8","DOI":"10.1007\/s10817-008-9103-8"},{"key":"19_CR9","doi-asserted-by":"publisher","unstructured":"Seto, D., Krogh, B., Sha, L., Chutinan, A.: The simplex architecture for safe online control system upgrades. In: Proceedings of the 1998 American Control Conference. ACC, vol.\u00a06, pp. 3504\u20133508 (1998). https:\/\/doi.org\/10.1109\/ACC.1998.703255","DOI":"10.1109\/ACC.1998.703255"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Slagel, J.T., Moscato, M.M., White, L., Mu\u00f1oz, C., Balachandran, S., Dutle, A.: Embedding differential dynamic logic in PVS. In: International Conference on Logical and Semantic Frameworks, with Applications. LSFA (2023). https:\/\/ntrs.nasa.gov\/citations\/20220019093","DOI":"10.4204\/EPTCS.402.7"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"White, L., Titolo, L., Slagel, J.T., Mu\u00f1oz, C.: A temporal differential dynamic logic formal embedding. In: ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP (2024). https:\/\/doi.org\/10.1145\/3636501.3636943","DOI":"10.1145\/3636501.3636943"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:04:34Z","timestamp":1716768274000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}