{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T17:06:20Z","timestamp":1761930380060,"version":"3.41.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031937057","type":"print"},{"value":"9783031937064","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-93706-4_2","type":"book-chapter","created":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:39Z","timestamp":1749316959000},"page":"11-30","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Process-Algebraic Semantics for\u00a0Verifying Intelligent Robotic Control Software"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4641-5354","authenticated-orcid":false,"given":"Ziggy","family":"Attala","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5603-3467","authenticated-orcid":false,"given":"Fang","family":"Yan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9889-9514","authenticated-orcid":false,"given":"Simon","family":"Foster","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0831-1976","authenticated-orcid":false,"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7955-2702","authenticated-orcid":false,"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,6,8]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Attala, Z., Cavalcanti, A.L.C., Woodcock, J.C.P.: Modelling and verifying robotic software that uses neural networks. In:\u00a0\u00c1brah\u00e1m, E.,\u00a0Dubslaff, C., Tarifa, S.L.T. (eds.) Theoretical Aspects of Computing, pp. 15\u201335. Springer, Heidelberg (2023)","DOI":"10.1007\/978-3-031-47963-2_3"},{"key":"2_CR2","unstructured":"Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend. Packt Publishing (2016)"},{"issue":"1","key":"2_CR3","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reason. 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reason."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Stell, A.: Verifying feedforward neural networks for classification in Isabelle\/HOL. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal Methods, pp. 427\u2013444. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-27481-7_24"},{"key":"2_CR5","unstructured":"Budinsky, F., Brodsky, S.A., Merks, E.: Eclipse Modeling Framework. Pearson Education, Boston (2003)"},{"key":"2_CR6","unstructured":"Cavalcanti, A., et al.: RoboSapiens WP1 D1.1 Report (Draft). https:\/\/robostar.cs.york.ac.uk\/publications\/reports\/Draft_RoboSapiensD1_1.pdf\u2019"},{"key":"2_CR7","unstructured":"CBMC - Bounded Model Checker for C and C++ programs (2024). http:\/\/www.cprover.org\/cprover-manual\/"},{"key":"2_CR8","unstructured":"Daggitt, M.L., Kokke, W., Atkey, R., Slusarz, N., Arnaboldi, L., Komendantskaya, E.: Vehicle: bridging the embedding gap in the verification of neuro-symbolic programs (2024)"},{"key":"2_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102510","volume":"197","author":"S Foster","year":"2020","unstructured":"Foster, S., Baxter, J., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying semantic foundations for automated verification tools in Isabelle\/UTP. Sci. Comput. Program. 197, 102510 (2020)","journal-title":"Sci. Comput. Program."},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.tcs.2019.09.017","volume":"802","author":"S Foster","year":"2020","unstructured":"Foster, S., Cavalcanti, A., Canham, S., Woodcock, J., Zeyda, F.: Unifying theories of reactive design contracts. Theor. Comput. Sci. 802, 105\u2013140 (2020)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100681","volume":"121","author":"S Foster","year":"2021","unstructured":"Foster, S., Ye, K., Cavalcanti, A., Woodcock, J.: Automated verification of reactive and concurrent programs by calculation. J. Logical Algebraic Methods Program. 121, 100681 (2021)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T.,\u00a0Armstrong, P.,\u00a0Boulgakov, A., Roscoe, A.W.: FDR3 - a modern refinement checker for CSP. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 187\u2013201 (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Henriksen, P.,\u00a0Lomuscio, A.: Efficient neural network verification via adaptive refinement and adversarial search. In: European Conference on Artificial Intelligence (2020)","DOI":"10.3233\/FAIA200385"},{"key":"2_CR14","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)"},{"key":"2_CR15","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Upper Saddle river (1998)"},{"key":"2_CR16","unstructured":"Isac, O., Barrett, C.W., Zhang, M., Katz, G.: Neural network verification with proof production. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 38\u201348 (2022)"},{"issue":"5s","key":"2_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3477023","volume":"20","author":"R Ivanov","year":"2021","unstructured":"Ivanov, R., Jothimurugan, K., Hsu, S., Vaidya, S., Alur, R., Bastani, O.: Compositional learning and verification of neural network controllers. ACM Trans. Embedded Comput. Syst. (TECS) 20(5s), 1\u201326 (2021)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/11787044_11","volume-title":"Model Driven Architecture \u2013 Foundations and Applications","author":"DS Kolovos","year":"2006","unstructured":"Kolovos, D.S., Paige, R.F., Polack, F.: The epsilon object language (EOL). In: Rensink, A., Warmer, J. (eds.) ECMDA-FA 2006. LNCS, vol. 4066, pp. 128\u2013142. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11787044_11"},{"key":"2_CR20","unstructured":"Kotha, S., Brix, C., Kolter, Z., Dvijotham, K., Zhang, H.: Provably bounding neural network preimages. In: Proceedings of the 37th International Conference on Neural Information Processing Systems, NIPS \u201923. Curran Associates Inc., Red Hook (2024)"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Lachnitt, H., et al.: IsaRare: automatic verification of SMT rewrites in isabelle\/HOL. In: Tools and Algorithms for the Construction and Analysis of Systems: 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, pp. 311\u2013330. Springer-Verlag, Heidelberg (2024)","DOI":"10.1007\/978-3-031-57246-3_17"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-642-35289-8_3","volume-title":"Neural Networks: Tricks of the Trade","author":"YA LeCun","year":"2012","unstructured":"LeCun, Y.A., Bottou, L., Orr, G.B., M\u00fcller, K.-R.: Efficient BackProp. In: Montavon, G., Orr, G.B., M\u00fcller, K.-R. (eds.) Neural Networks: Tricks of the Trade. LNCS, vol. 7700, pp. 9\u201348. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35289-8_3"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: Nnv 2.0: the neural network verification tool. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 397\u2013412. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37703-7_19"},{"key":"2_CR24","unstructured":"The MathWorks, Inc. Simulink. www.mathworks.com\/products\/simulink"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., et al.: Diagrammatic physical robot models. Accepted for publication in Softw. Syst. Model (2024)","DOI":"10.1007\/s10270-025-01270-9"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"2_CR27","unstructured":"Oliveira, M.V.M.: Formal Derivation of State-Rich Reactive Programs Using Circus. PhD thesis, University of York (2006)"},{"issue":"1","key":"2_CR28","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1002\/inst.12434","volume":"26","author":"R Raman","year":"2023","unstructured":"Raman, R., Gupta, N., Jeppu, Y.: Framework for formal verification of machine learning based complex system-of-systems. Insight 26(1), 91\u2013102 (2023)","journal-title":"Insight"},{"key":"2_CR29","unstructured":"Simulink Design Verifier (2024). https:\/\/www.mathworks.com\/products\/simulink-design-verifier.html"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC \u201919, pp. 147\u2013156. Association for Computing Machinery, New York (2019)","DOI":"10.1145\/3302504.3311802"},{"key":"2_CR31","unstructured":"University of York. RoboChart Reference Manual. www.cs.york.ac.uk\/circus\/RoboCalc\/robotool\/"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Viyovi\u0107, V., Maksimovi\u0107, M., Perisi\u0107, B.: Sirius: a rapid development of DSM graphical editor. In: IEEE 18th International Conference on Intelligent Engineering Systems INES 2014, pp. 233\u2013238 (2014)","DOI":"10.1109\/INES.2014.6909375"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-030-31038-7_5","volume-title":"Unifying Theories of Programming","author":"J Woodcock","year":"2019","unstructured":"Woodcock, J., Cavalcanti, A., Foster, S., Mota, A., Ye, K.: Probabilistic semantics for RoboChart. In: Ribeiro, P., Sampaio, A. (eds.) UTP 2019. LNCS, vol. 11885, pp. 80\u2013105. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31038-7_5"},{"key":"2_CR34","unstructured":"Woodcock, J.C.P.,\u00a0Davies, J.: Using Z - Specification, Refinement, and Proof. Prentice-Hall (1996)"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Zhang, Z., Wu, Y., Liu, S., Liu, J., Zhang, M.: Provably tightest linear approximation for robustness verification of sigmoid-like neural networks. In: Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE \u201922. Association for Computing Machinery, New York (2023)","DOI":"10.1145\/3551349.3556907"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Zhi, D., Wang, P., Liu, S.,\u00a0Luke Ong, C.-H., Zhang, M.: Unifying qualitative and quantitative safety verification of DNN-controlled systems. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 401\u2013426. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65630-9_20"}],"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-93706-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:22:46Z","timestamp":1749316966000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-93706-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031937057","9783031937064"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-93706-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"8 June 2025","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":"Hampton Roads, VA","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}