{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T13:36:58Z","timestamp":1760189818917,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031077265"},{"type":"electronic","value":"9783031077272"}],"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-07727-2_1","type":"book-chapter","created":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T01:12:12Z","timestamp":1654045932000},"page":"3-17","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Autonomous Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1426-1896","authenticated-orcid":false,"given":"Louise A.","family":"Dennis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,6,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B. Cambridge University Press, London (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-319-30734-3_6","volume-title":"Theory and Practice of Formal Methods","author":"D Ancona","year":"2016","unstructured":"Ancona, D., Ferrando, A., Mascardi, V.: Comparing trace expressions and linear temporal logic for runtime verification. In: \u00c1brah\u00e1m, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 47\u201364. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30734-3_6"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL \u2014 a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bordini, R.H., H\u00fcbner, J.F., Wooldridge, M.: Programming Multi-agent Systems in AgentSpeak Using Jason. John Wiley & Sons, Chichester (2007)","DOI":"10.1002\/9780470061848"},{"key":"1_CR6","unstructured":"Boyer, R.S., Strother Moore, J. (eds.): The Correctness Problem in Computer Science. Academic Press, New York (1981)"},{"key":"1_CR7","unstructured":"Bratman, M.E.: Intentions, Plans, and Practical Reason. Harvard University Press, Cambridge (1987)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Cardoso, R.C., Dennis, L.A., Farrell, M., Fisher, M., Luckcuck, M.: Towards compositional verification for modular robotic systems. In: Proceedings 2nd International Workshop on Formal Methods for Autonomous Systems (FMAS 2020) (2020)","DOI":"10.4204\/EPTCS.329.2"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Cardoso, R.C., Farrell, M., Luckcuck, M., Ferrando, A., Fisher, M.: Heterogeneous verification of an autonomous curiosity rover. In: Proc. 12th International NASA Formal Methods Symposium (NFM). LNCS, vol. 12229, pp. 353\u2013360. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6","DOI":"10.1007\/978-3-030-55754-6"},{"key":"1_CR10","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"1_CR11","series-title":"Multiagent Systems, Artificial Societies, and Simulated Organizations","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/0-387-26350-0_2","volume-title":"Multi-Agent Programming","author":"M Dastani","year":"2005","unstructured":"Dastani, M., van Birna Riemsdijk, M., Meyer, J.-J.C.: Programming multi-agent systems in 3APL. In: Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.) Multi-Agent Programming. MSASSO, vol. 15, pp. 39\u201367. Springer, Boston, MA (2005). https:\/\/doi.org\/10.1007\/0-387-26350-0_2"},{"issue":"5","key":"1_CR12","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"RA DeMillo","year":"1979","unstructured":"DeMillo, R.A., Lipton, R.J., Perlis, A.: Social processes and proofs of theorems of programs. ACM Commun. 22(5), 271\u2013280 (1979)","journal-title":"ACM Commun."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Dennis, L.A.: The mcapl framework including the agent infrastructure layer and agent Java Pathfinder. J. Open Source Softw. 3(24) (2018)","DOI":"10.21105\/joss.00617"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-030-66494-7_7","volume-title":"Software Engineering for Robotics","author":"L Dennis","year":"2021","unstructured":"Dennis, L., Fisher, M.: Verifiable autonomy and responsible robotics. In: Software Engineering for Robotics, pp. 189\u2013217. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-66494-7_7"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Dennis, L.A., Fisher, M., Lincoln, N.K., Lisitsa, A., Veres, S.M.: Practical Verification of decision-making in agent-based autonomous systems. Autom. Softw. Eng. 23(3), 305\u2013359 (2016). https:\/\/doi.org\/10.1007\/s10515-014-0168-9","DOI":"10.1007\/s10515-014-0168-9"},{"issue":"1","key":"1_CR16","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L.A., Fisher, M., Webster, M., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5\u201363 (2012)","journal-title":"Autom. Softw. Eng."},{"key":"1_CR17","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A Tutorial on runtime verification. In: Engineering Dependable Software Systems, pp. 141\u2013175. IOS Press, Amsterdam (2013)"},{"key":"1_CR18","unstructured":"Farrell, M., et al.: Modular verification of autonomous space robotics (2019)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-03769-7_15","volume-title":"Runtime Verification","author":"A Ferrando","year":"2018","unstructured":"Ferrando, A., Dennis, L.A., Ancona, D., Fisher, M., Mascardi, V.: Verifying and validating autonomous systems: towards an integrated approach. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 263\u2013281. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_15"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Ferrando, A., Dennis, L.A., Cardoso, R.C., Fisher, M., Ancona, D., Mascardi, V.: Toward a holistic approach to verification and validation of autonomous cognitive systems. ACM Trans. Softw. Eng. Methodol. 30(4), 43:1\u201343:43 (2021). https:\/\/doi.org\/10.1145\/3447246","DOI":"10.1145\/3447246"},{"issue":"9","key":"1_CR21","doi-asserted-by":"publisher","first-page":"1048","DOI":"10.1145\/48529.48530","volume":"31","author":"JH Fetzer","year":"1988","unstructured":"Fetzer, J.H.: Program verification: the very idea. ACM Commun. 31(9), 1048\u20131063 (1988)","journal-title":"ACM Commun."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Garoche, P.L.: Formal Verification of Control System Software. Princeton University Press (2019), http:\/\/www.jstor.org\/stable\/j.ctv80cd4v","DOI":"10.23943\/princeton\/9780691181301.001.0001"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-0-387-89299-3_4","volume-title":"Multi-Agent Programming","author":"KV Hindriks","year":"2009","unstructured":"Hindriks, K.V.: Programming rational agents in GOAL. In: El Fallah Seghrouchni, A., Dix, J., Dastani, M., Bordini, R.H. (eds.) Multi-Agent Programming, pp. 119\u2013157. Springer, Boston, MA (2009). https:\/\/doi.org\/10.1007\/978-0-387-89299-3_4"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Howey, R., Long, D., Fox, M.: VAL: Automatic plan validation, continuous effects and mixed initiative planning using PDDL. In: Proceedings of the ICTAI, pp. 294\u2013301 (2004). https:\/\/doi.org\/10.1109\/ICTAI.2004.120","DOI":"10.1109\/ICTAI.2004.120"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Huang, X., et al.: A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability. Comput. Sci. Rev. 37, 100270 (2020). https:\/\/doi.org\/10.1016\/j.cosrev.2020.100270, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1574013719302527","DOI":"10.1016\/j.cosrev.2020.100270"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Kamali, M., Dennis, L.A., McAree, O., Fisher, M., Veres, S.M.: Formal verification of autonomous vehicle platooning. Sci. Comput. Program. 148, 88\u2013106 (2017). http:\/\/arxiv.org\/abs\/1602.01718","DOI":"10.1016\/j.scico.2017.05.006"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Lacerda, B., Faruq, F., Parker, D., Hawes, N.: Probabilistic planning with formal performance guarantees for mobile service robots. Int. J. Robot. Res. 38(9) (2019). https:\/\/doi.org\/10.1177\/0278364919856695","DOI":"10.1177\/0278364919856695"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Mehlitz, P.C., Rungta, N., Visser, W.: A hands-on Java PathFinder tutorial. In: Proceedings of the 35th International Conference on Software Engineering (ICSE), pp. 1493\u20131495. IEEE\/ACM (2013). http:\/\/dl.acm.org\/citation.cfm?id=2486788","DOI":"10.1109\/ICSE.2013.6606756"},{"key":"1_CR29","series-title":"Multiagent Systems, Artificial Societies, and Simulated Organizations","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/0-387-26350-0_6","volume-title":"Multi-Agent Programming","author":"A Pokahr","year":"2005","unstructured":"Pokahr, A., Braubach, L., Lamersdorf, W.: Jadex: a BDI reasoning engine. In: Bordini, R.H., Dastani, M., Dix, J., El Fallah Seghrouchni, A. (eds.) Multi-Agent Programming. MSASSO, vol. 15, pp. 149\u2013174. Springer, Boston, MA (2005). https:\/\/doi.org\/10.1007\/0-387-26350-0_6"},{"key":"1_CR30","unstructured":"Quigley, M., et al.: ROS: an open-source robot operating system. In: Proceedings of the ICRA Workshop on Open Source Software (2009)"},{"key":"1_CR31","unstructured":"Raimondi, F., Pecheur, C., Brat, G.: PDVer, a tool to verify PDDL planning domains. In: Proceedings of the ICAPS 2009 (2009). http:\/\/lvl.info.ucl.ac.be\/Publications\/PDVerAToolToVerifyPDDLPlanningDomains"},{"key":"1_CR32","unstructured":"Rao, A.S., Georgeff, M.P.: Modeling agents within a BDI-architecture. In: Proceedings of the 2nd International Conference Principles of Knowledge Representation and Reasoning (KR&R), pp. 473\u2013484. Morgan Kaufmann (1991)"},{"key":"1_CR33","unstructured":"Rao, A.S., Georgeff, M.P.: An abstract architecture for rational agents. In: Proceedings of the International Conference Knowledge Representation and Reasoning (KR&R), pp. 439\u2013449. Morgan Kaufmann (1992)"},{"key":"1_CR34","unstructured":"Rao, A.S., Georgeff, M.P.: BDI agents: from theory to practice. In: Proceedings of the 1st International Conference on Multi-Agent Systems (ICMAS), pp. 312\u2013319. San Francisco, USA (1995)"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/BFb0031845","volume-title":"Agents Breaking Away","author":"AS Rao","year":"1996","unstructured":"Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: Van de Velde, W., Perram, J.W. (eds.) MAAMAW 1996. LNCS, vol. 1038, pp. 42\u201355. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031845"},{"issue":"2","key":"1_CR36","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","volume":"12","author":"G Rosu","year":"2005","unstructured":"Rosu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151\u2013197 (2005)","journal-title":"Autom. Softw. Eng."},{"issue":"2","key":"1_CR37","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Automat. Softw. Eng. 10(2), 203\u2013232 (2003)","journal-title":"Automat. Softw. Eng."},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Visser, W., Mehlitz, P.C.: Model Checking Programs with Java PathFinder. In: Proceedings 12th International SPIN Workshop. LNCS, vol.\u00a03639, p.\u00a027. Springer, Cham (2005)","DOI":"10.1007\/11537328_5"},{"key":"1_CR39","unstructured":"Wooldridge, M.: An Introduction to Multiagent Systems. John Wiley & Sons, Chichester (2002)"},{"volume-title":"Foundations of Rational Agency","year":"1999","key":"1_CR40","unstructured":"Wooldridge, M., Rao, A. (eds.): Foundations of Rational Agency. Kluwer Academic Publishers, Applied Logic Series (1999)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-07727-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,7]],"date-time":"2022-06-07T19:19:43Z","timestamp":1654629583000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-07727-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031077265","9783031077272"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-07727-2_1","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":"1 June 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lugano","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Switzerland","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":"7 June 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2022","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":"ifm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ifmconference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Also includes: 1 abstract of an invited talk, 2 invited papers, 7 extended abstracts of presentations accepted at PhD symposium","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}