{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T04:23:53Z","timestamp":1774671833516,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T00:00:00Z","timestamp":1602028800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S001190\/1"],"award-info":[{"award-number":["EP\/S001190\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,7]]},"DOI":"10.1145\/3372020.3391559","type":"proceedings-article","created":{"date-parts":[[2020,9,12]],"date-time":"2020-09-12T20:02:05Z","timestamp":1599940925000},"page":"11-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Formal Model-Based Assurance Cases in Isabelle\/SACM"],"prefix":"10.1145","author":[{"given":"Simon","family":"Foster","sequence":"first","affiliation":[{"name":"University of York"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yakoub","family":"Nemouchi","sequence":"additional","affiliation":[{"name":"University of York"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"O'Halloran","sequence":"additional","affiliation":[{"name":"D-RisQ Software Systems"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karen","family":"Stephenson","sequence":"additional","affiliation":[{"name":"D-RisQ Software Systems"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nick","family":"Tudor","sequence":"additional","affiliation":[{"name":"D-RisQ Software Systems"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"A. Armstrong V. Gomes and G. Struth. 2015. Building program construction and verification tools from algebraic principles. Formal Aspects of Computing 28 2 (2015). A. Armstrong V. Gomes and G. Struth. 2015. Building program construction and verification tools from algebraic principles. Formal Aspects of Computing 28 2 (2015).","DOI":"10.1007\/s00165-015-0343-1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_3_2_1_3_1","volume-title":"Using the Isabelle Ontology Framework - Linking the Formal with the Informal. In Intelligent Computer Mathematics (CICM) (LNCS)","volume":"11006","author":"Brucker A."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"A. Brucker and B. Wolff. 2019. Isabelle\/DOF: Design and Implementation. In SEFM (LNCS 11724). Springer 279--292. A. Brucker and B. Wolff. 2019. Isabelle\/DOF: Design and Implementation. In SEFM (LNCS 11724). Springer 279--292.","DOI":"10.1007\/978-3-030-30446-1_15"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"A. Brucker and B. Wolff. 2019. Using Ontologies in Formal Developments Targeting Certification. In Integrated Formal Methods (iFM) (LNCS) Vol. 11918. Springer 65--82. A. Brucker and B. Wolff. 2019. Using Ontologies in Formal Developments Targeting Certification. In Integrated Formal Methods (iFM) (LNCS) Vol. 11918. Springer 65--82.","DOI":"10.1007\/978-3-030-34968-4_4"},{"key":"e_1_3_2_1_6_1","volume-title":"Tool Integration with the Evidential Tool Bus. In VMCAI (LNCS)","volume":"7737","author":"Cruanes S."},{"key":"e_1_3_2_1_7_1","volume-title":"SAFECOMP (LNCS)","volume":"8153","author":"Denney E."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","unstructured":"E. Denney and G. Pai. 2015. Towards a Formal Basis for Modular Safety Cases. In Computer Safety Reliability and Security (SAFECOMP) (LNCS) Vol. 9337. Springer 328--343. E. Denney and G. Pai. 2015. Towards a Formal Basis for Modular Safety Cases. In Computer Safety Reliability and Security (SAFECOMP) (LNCS) Vol. 9337. Springer 328--343.","DOI":"10.1007\/978-3-319-24255-2_24"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3269687.3269695"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_11_1","volume-title":"Hybrid Relations in Isabelle\/UTP. In 7th Intl. Symp. on Unifying Theories of Programming (UTP) (LNCS)","volume":"11885","author":"Foster S.","year":"2019"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"S. Foster J. Baxter A. Cavalcanti A. Miyazawa and J. Woodcock. 2018. Automating Verification of State Machines with Reactive Designs and Isabelle\/UTP. In FACS (LNCS 11222). Springer 137--155. S. Foster J. Baxter A. Cavalcanti A. Miyazawa and J. Woodcock. 2018. Automating Verification of State Machines with Reactive Designs and Isabelle\/UTP. In FACS (LNCS 11222). Springer 137--155.","DOI":"10.1007\/978-3-030-02146-7_7"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"S. Foster A. Cavalcanti S. Canham J. Woodcock and F. Zeyda. 2020. Unifying Theories of Reactive Design Contracts. Theoretical Computer Science 802 (January 2020) 105--140. S. Foster A. Cavalcanti S. Canham J. Woodcock and F. Zeyda. 2020. Unifying Theories of Reactive Design Contracts. Theoretical Computer Science 802 (January 2020) 105--140.","DOI":"10.1016\/j.tcs.2019.09.017"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","unstructured":"S. Foster Y. Nemouchi M. Gleirscher and T. Kelly. 2019. Isabelle\/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. In iFM (LNCS 11918). Springer 379--398. S. Foster Y. Nemouchi M. Gleirscher and T. Kelly. 2019. Isabelle\/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods. In iFM (LNCS 11918). Springer 379--398.","DOI":"10.1007\/978-3-030-34968-4_21"},{"key":"e_1_3_2_1_15_1","volume-title":"Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. In Proc. 17th Intl. Conf. on Relational and Algebraic Methods in Computer Science (RAMICS) (LNCS)","volume":"11194","author":"Foster S."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"S. Foster F. Zeyda and J. Woodcock. 2016. Unifying heterogeneous state-spaces with lenses. In ICTAC (LNCS 9965). Springer 295--314. S. Foster F. Zeyda and J. Woodcock. 2016. Unifying heterogeneous state-spaces with lenses. In ICTAC (LNCS 9965). Springer 295--314.","DOI":"10.1007\/978-3-319-46750-4_17"},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (HILT). ACM, 19--28","author":"Gacek A."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"M. Gleirscher S. Foster and Y. Nemouchi. 2019. Evolution of Formal Model-Based Assurance Cases for Autonomous Robots. In SEFM (LNCS 11724). Springer 87--104. M. Gleirscher S. Foster and Y. Nemouchi. 2019. Evolution of Formal Model-Based Assurance Cases for Autonomous Robots. In SEFM (LNCS 11724). Springer 87--104.","DOI":"10.1007\/978-3-030-30446-1_5"},{"key":"e_1_3_2_1_19_1","first-page":"36","article-title":"New Opportunities for Integrated Formal","volume":"52","author":"Gleirscher M.","year":"2019","journal-title":"Methods. Comput. Surveys"},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). ACM, 429--439","author":"Greenaway G."},{"key":"e_1_3_2_1_21_1","volume-title":"Balancing the Formal and Informal in Safety Case Arguments. In VeriSure Workshop, colocated with CAV.","author":"Habli I."},{"key":"e_1_3_2_1_22_1","volume-title":"18th International Conference, TPHOLs 2005 (August 2005)","volume":"3603","author":"Harrison J.","year":"2005"},{"key":"e_1_3_2_1_23_1","volume-title":"Proc. 16th Intl. Symp. on High Assurance Systems Engineering. IEEE.","author":"Hawkins R."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare and J. He. 1998. Unifying Theories of Programming. Prentice-Hall. C. A. R. Hoare and J. He. 1998. Unifying Theories of Programming. Prentice-Hall.","DOI":"10.1007\/BFb0002714"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_9"},{"key":"e_1_3_2_1_26_1","volume-title":"Numerical Analysis of Ordinary Differential Equations in Isabelle\/HOL. In 3rd Intl. Conf. on Interactive Theorem Proving (ITP) (LNCS)","volume":"7406","author":"Immler F."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"A. Miyazawa P. Ribeiro W. Li A. Cavalcanti J. Timmis and J. Woodcock. 2019. RoboChart: modelling and verification of the functional behaviour of robotic applications. Software and Systems Modelling 18 (January 2019) 3097--3149. Issue 5. A. Miyazawa P. Ribeiro W. Li A. Cavalcanti J. Timmis and J. Woodcock. 2019. RoboChart: modelling and verification of the functional behaviour of robotic applications. Software and Systems Modelling 18 (January 2019) 3097--3149. Issue 5.","DOI":"10.1007\/s10270-018-00710-z"},{"key":"e_1_3_2_1_29_1","volume-title":"Automatic Property Checking of Robotic Applications. In Intl. Conf. on Intelligent Robots and Systems (IROS). IEEE, 3869--3876","author":"Miyazawa A."},{"key":"e_1_3_2_1_30_1","volume-title":"Programming from Specifications","author":"Morgan C."},{"key":"e_1_3_2_1_31_1","volume-title":"Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle\/HOL. In 18th Intl. Conf on Relational and Algebraic Methods in Computer Science (RAMiCS) (LNCS)","volume":"12062","author":"Munive J. H. Y."},{"key":"e_1_3_2_1_32_1","volume-title":"Proc. 2014 Haskell Symposium. ACM","author":"Muranushi T."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0052-5"},{"key":"e_1_3_2_1_34_1","volume-title":"Logical Foundations of Cyber-Physical Systems"},{"key":"e_1_3_2_1_35_1","volume-title":"Formal Methods and Software Engineering (ICFEM) (LNCS)","author":"Rushby J."},{"key":"e_1_3_2_1_36_1","volume-title":"The Z-Notation - A Reference Manual","author":"Spivey M."},{"key":"e_1_3_2_1_37_1","first-page":"13","article-title":"Deeply Integrating C11 Code Support into Isabelle\/PIDE","volume":"310","author":"Tuong F.","year":"2019","journal-title":"Formal Integrated Development Environment (F-IDE) (EPTCS)"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"R. Wei T. Kelly X. Dai S. Zhao and R. Hawkins. 2019. Model based system assurance using the Structured Assurance Case Metamodel. Systems and Software 154 (2019). R. Wei T. Kelly X. Dai S. Zhao and R. Hawkins. 2019. Model based system assurance using the Structured Assurance Case Metamodel. Systems and Software 154 (2019).","DOI":"10.1016\/j.jss.2019.05.013"},{"key":"e_1_3_2_1_39_1","volume-title":"CICM (LNCS 11617)","author":"Wenzel M."},{"key":"e_1_3_2_1_40_1","volume-title":"Probabilistic Semantics for RoboChart. In 7th Intl. Symp. on Unifying Theories of Programming (UTP) (LNCS)","volume":"11885","author":"Woodcock J."}],"event":{"name":"FormaliSE '20: 8th International Conference on Formal Methods in Software Engineering","location":"Seoul Republic of Korea","acronym":"FormaliSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 8th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391559","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372020.3391559","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:19Z","timestamp":1750203859000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391559"}},"subtitle":["An Autonomous Underwater Vehicle Case Study"],"short-title":[],"issued":{"date-parts":[[2020,10,7]]},"references-count":39,"alternative-id":["10.1145\/3372020.3391559","10.1145\/3372020"],"URL":"https:\/\/doi.org\/10.1145\/3372020.3391559","relation":{},"subject":[],"published":{"date-parts":[[2020,10,7]]},"assertion":[{"value":"2020-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}