{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T17:41:54Z","timestamp":1749318114628,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031479625"},{"type":"electronic","value":"9783031479632"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-47963-2_3","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:41:26Z","timestamp":1700689286000},"page":"15-35","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Modelling and\u00a0Verifying Robotic Software that\u00a0Uses Neural Networks"],"prefix":"10.1007","author":[{"given":"Ziggy","family":"Attala","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,23]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.apor.2012.05.008","volume":"37","author":"J-H Ahn","year":"2012","unstructured":"Ahn, J.-H., Rhee, K., You, Y.: A study on the collision avoidance of a ship using neural networks and fuzzy logic. Appl. Ocean Res. 37, 162\u2013173 (2012)","journal-title":"Appl. Ocean Res."},{"key":"3_CR2","unstructured":"An, P.E., Harris, C.J., Tribe, R., Clarke, N.: Aspects of neural networks in intelligent collision avoidance systems for prometheus. In: Joint Framework for Information Technology, pp. 129\u2013135 (1993)"},{"key":"3_CR3","unstructured":"Attala, Z.: Verification of RoboChart models with ANN components. Technical report, University of York (2023). https:\/\/robostar.cs.york.ac.uk\/publications\/reports\/Ziggy_Attala_Draft_Thesis.pdf"},{"key":"3_CR4","unstructured":"Attala, Z., Cavalcanti, A.L.C., Woodcock, J.C.P.: A comparison of neural network tools for the verification of linear specifications of ReLU networks. In: Albarghouthi, A., Katz, G., Narodytska, N. (eds.) 3rd Workshop on Formal Methods for ML-Enabled Autonomous System, pp. 22\u201333 (2020)"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-031-27481-7_24","volume-title":"Formal Methods","author":"AD Brucker","year":"2023","unstructured":"Brucker, A.D., Stell, A.: Verifying feedforward neural networks for classification in Isabelle\/HOL. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 427\u2013444. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_24"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Clavi\u00e8re, A., Asselin, E., Garion, C., Pagetti, C.: Safety verification of neural network controlled systems. CoRR, abs\/2011.05174 (2020)","DOI":"10.1109\/DSN-W52860.2021.00019"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Dreossi, T., et al.: Counterexample-guided data augmentation. arXiv:1805.06962 (2018)","DOI":"10.24963\/ijcai.2018\/286"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-030-88885-5_21","volume-title":"Automated Technology for Verification and Analysis","author":"G Dupont","year":"2021","unstructured":"Dupont, G., A\u00eft-Ameur, Y., Pantel, M., Singh, N.K.: Event-B refinement for continuous behaviours approximation. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 320\u2013336. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_21"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Foster, S., Baxter, J., Cavalcanti, A.L.C., Woodcock, J.C.P., Zeyda, F.: Unifying semantic foundations for automated verification tools in Isabelle\/UTP. Sci. Comput. Program. 197, 102510 (2020)","DOI":"10.1016\/j.scico.2020.102510"},{"key":"3_CR10","unstructured":"Foster, S., et al.: Unifying theories of reactive design contracts. CoRR, abs\/1712.10233 (2017)"},{"key":"3_CR11","unstructured":"Foster, S., et al.: Automated verification of reactive and concurrent programs by calculation. CoRR, abs\/2007.13529 (2020)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3\u2014a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"key":"3_CR13","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliff (1998)"},{"key":"3_CR14","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International, Englewood Cliff (1985)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"2015","DOI":"10.1007\/s00521-020-05097-x","volume":"33","author":"VJ Hodge","year":"2020","unstructured":"Hodge, V.J., Hawkins, R., Alexander, R.: Deep reinforcement learning for drone navigation using sensor data. Neural Comput. Appl. 33, 2015\u20132033 (2020). https:\/\/doi.org\/10.1007\/s00521-020-05097-x","journal-title":"Neural Comput. Appl."},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Hu, B.C., et al.: If a human can see it, so should your system. In: Proceedings of the 44th International Conference on Software Engineering. ACM (2022)","DOI":"10.1145\/3510003.3510109"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Jacoby, Y., Barrett, C.W., Katz, G.: Verifying recurrent neural networks using invariant inference. CoRR, abs\/2004.02462 (2020)","DOI":"10.1007\/978-3-030-59152-6_3"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Julian, K.D., Kochenderfer, M.J.: Guaranteeing safety for neural network-based aircraft collision avoidance systems. In: 2019 IEEE\/AIAA 38th Digital Avionics Systems Conference (DASC). IEEE (2019)","DOI":"10.1109\/DASC43569.2019.9081748"},{"issue":"3","key":"3_CR19","doi-asserted-by":"publisher","first-page":"598","DOI":"10.2514\/1.G003724","volume":"42","author":"KD Julian","year":"2019","unstructured":"Julian, K.D., Kochenderfer, M.J., Owen, M.P.: Deep neural network compression for aircraft collision avoidance systems. J. Guid. Control. Dyn. 42(3), 598\u2013608 (2019)","journal-title":"J. Guid. Control. Dyn."},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"3_CR21","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":"3_CR22","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1038\/nature14539","volume":"521","author":"Y LeCun","year":"2015","unstructured":"LeCun, Y., Bengio, Y., Hinton, G.: Deep learning. Nature 521, 436\u2013444 (2015). https:\/\/doi.org\/10.1038\/nature14539","journal-title":"Nature"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-319-10181-1_10","volume-title":"Integrated Formal Methods","author":"A Miyazawa","year":"2014","unstructured":"Miyazawa, A., Cavalcanti, A.: Formal refinement in SysML. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 155\u2013170. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_10"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18, 3097\u20133149 (2019)","journal-title":"Softw. Syst. Model."},{"key":"3_CR25","series-title":"Lecture Notes in Civil Engineering","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-319-67443-8_5","volume-title":"Experimental Vibration Analysis for Civil Structures","author":"AC Neves","year":"2018","unstructured":"Neves, A.C., Gonz\u00e1lez, I., Leander, J., Karoumi, R.: A new approach to damage detection in bridges using machine learning. In: Conte, J.P., Astroza, R., Benzoni, G., Feltrin, G., Loh, K.J., Moaveni, B. (eds.) EVACES 2017. LNCE, vol. 5, pp. 73\u201384. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-67443-8_5"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-319-11900-7_17","volume-title":"Simulation, Modeling, and Programming for Autonomous Robots","author":"A Nordmann","year":"2014","unstructured":"Nordmann, A., Hochgeschwender, N., Wrede, S.: A survey on domain-specific languages in robotics. In: Brugali, D., Broenink, J.F., Kroeger, T., MacDonald, B.A. (eds.) SIMPAR 2014. LNCS (LNAI), vol. 8810, pp. 195\u2013206. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11900-7_17"},{"key":"3_CR27","unstructured":"Nwankpa, C., et al.: Activation functions: comparison of trends in practice and research for deep learning. arXiv:1811.03378 (2018)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Austin, P.D., Welch, P.H.: CSP for JavaTM (JCSP) 1.1-RC4 API specification (2008). https:\/\/www.cs.kent.ac.uk\/projects\/ofa\/jcsp\/jcsp-1.1-rc4\/jcsp-doc\/","DOI":"10.1123\/jcsp.1.1.1"},{"key":"3_CR29","unstructured":"ProofPower-Z reference manual (2006)"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Rojas, R.: Neural Networks \u2013 A Systematic Introduction, chap. 7. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/978-3-642-61068-4","DOI":"10.1007\/978-3-642-61068-4"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science. Springer, London (2011). https:\/\/doi.org\/10.1007\/978-1-84882-258-0","DOI":"10.1007\/978-1-84882-258-0"},{"key":"3_CR32","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliff (1997)"},{"key":"3_CR33","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol. 31, pp. 10802\u201310813. Curran Associates Inc. (2018)"},{"key":"3_CR34","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall, Englewood Cliff (1992)"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1007\/978-3-030-30942-8_39","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"H-D Tran","year":"2019","unstructured":"Tran, H.-D., et al.: Star-based reachability analysis of deep neural networks. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 670\u2013686. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_39"},{"key":"3_CR36","unstructured":"University of Oxford. FDR Manual, May 2020. Release 4.2.7. dl.cocotec.io\/fdr\/fdr-manual.pdf. Accessed 31 May 2020"},{"key":"3_CR37","unstructured":"Woodcock, J., Davies, J.: Using Z. Prentice Hall, Englewood Cliff (1996)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-030-88701-8_28","volume-title":"Relational and Algebraic Methods in Computer Science","author":"K Ye","year":"2021","unstructured":"Ye, K., Foster, S., Woodcock, J.: Automated reasoning for probabilistic sequential programs with theorem proving. In: Fahrenberg, U., Gehrke, M., Santocanale, L., Winter, M. (eds.) RAMiCS 2021. LNCS, vol. 13027, pp. 465\u2013482. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88701-8_28"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47963-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:41:40Z","timestamp":1700689300000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47963-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031479625","9783031479632"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47963-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"23 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Peru","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 December 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2023.compsust.utec.edu.pe\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}