{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T03:50:31Z","timestamp":1791345031922,"version":"4.3.1"},"reference-count":77,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,11,1]],"date-time":"2026-11-01T00:00:00Z","timestamp":1793491200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,11,1]],"date-time":"2026-11-01T00:00:00Z","timestamp":1793491200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,8,5]],"date-time":"2026-08-05T00:00:00Z","timestamp":1785888000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R026173"],"award-info":[{"award-number":["EP\/R026173"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R026092"],"award-info":[{"award-number":["EP\/R026092"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R026084"],"award-info":[{"award-number":["EP\/R026084"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V026801"],"award-info":[{"award-number":["EP\/V026801"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000287","name":"Royal Academy of Engineering","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000287","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Robotics and Autonomous Systems"],"published-print":{"date-parts":[[2026,11]]},"DOI":"10.1016\/j.robot.2026.105648","type":"journal-article","created":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T15:16:12Z","timestamp":1785424572000},"page":"105648","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["A compositional approach to verifying modular robotic systems"],"prefix":"10.1016","volume":"205","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6444-9312","authenticated-orcid":false,"given":"Matt","family":"Luckcuck","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7708-3877","authenticated-orcid":false,"given":"Marie","family":"Farrell","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8711-4670","authenticated-orcid":false,"given":"Angelo","family":"Ferrando","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6666-6954","authenticated-orcid":false,"given":"Rafael C.","family":"Cardoso","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1426-1896","authenticated-orcid":false,"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0875-3862","authenticated-orcid":false,"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.robot.2026.105648_b1","series-title":"Explainable Robotic Systems Workshop, ACM Human-Robot Interaction Conference","first-page":"2","article-title":"The ORCA Hub: Explainable offshore robotics through intelligent interfaces","author":"Hastie","year":"2018"},{"issue":"2","key":"10.1016\/j.robot.2026.105648_b2","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1108\/01439911111106327","article-title":"Robots in the nuclear industry: A review of technologies and applications","volume":"38","author":"Bogue","year":"2011","journal-title":"Ind. Robot.: An Int. J."},{"issue":"6","key":"10.1016\/j.robot.2026.105648_b3","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1109\/MIS.2018.111144814","article-title":"Autonomous Nuclear Waste Management","volume":"33","author":"Aitken","year":"2018","journal-title":"IEEE Intell. Syst."},{"issue":"2","key":"10.1016\/j.robot.2026.105648_b4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF00058762","article-title":"Robotic vehicles for planetary exploration","volume":"2","author":"Wilcox","year":"1992","journal-title":"Appl. Intell."},{"key":"10.1016\/j.robot.2026.105648_b5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.paerosci.2014.03.002","article-title":"A review of space robotics technologies for on-orbit servicing","volume":"68","author":"Flores-Abad","year":"2014","journal-title":"Prog. Aerosp. Sci."},{"key":"10.1016\/j.robot.2026.105648_b6","series-title":"Workshop on Open Source Software","article-title":"ROS: an open-source Robot Operating System","author":"Quigley","year":"2009"},{"key":"10.1016\/j.robot.2026.105648_b7","series-title":"Formal Verification of the Functional Layer of Robotic and Autonomous Systems","author":"Foughali","year":"2018"},{"key":"10.1016\/j.robot.2026.105648_b8","series-title":"International Conference on Intelligent Robots and Systems","first-page":"842","article-title":"GenoM: A tool for the specification and the implementation of operating modules in a distributed robot architecture","author":"Fleury","year":"1997"},{"key":"10.1016\/j.robot.2026.105648_b9","series-title":"Workshop on Formal Methods in Software Engineering","article-title":"Formal verification of ROS-based robotic applications using timed-automata","author":"Halder","year":"2017"},{"issue":"5","key":"10.1016\/j.robot.2026.105648_b10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3342355","article-title":"Formal specification and verification of autonomous robotic systems: A survey","volume":"52","author":"Luckcuck","year":"2019","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/j.robot.2026.105648_b11","series-title":"Model Checking","author":"Clarke","year":"1999"},{"issue":"5","key":"10.1016\/j.robot.2026.105648_b12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","article-title":"A brief account of runtime verification","volume":"78","author":"Leucker","year":"2009","journal-title":"J. Log. Algebraic Methods Program."},{"key":"10.1016\/j.robot.2026.105648_b13","series-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: the Calculus of Inductive Constructions","author":"Bertot","year":"2013"},{"key":"10.1016\/j.robot.2026.105648_b14","series-title":"Integrated Formal Methods","first-page":"161","article-title":"Robotics and Integrated Formal Methods: Necessity Meets Opportunity","volume":"vol. 11023","author":"Farrell","year":"2018"},{"issue":"4","key":"10.1016\/j.robot.2026.105648_b15","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","article-title":"Tentative steps toward a development method for interfering programs","volume":"5","author":"Jones","year":"1983","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"10","key":"10.1016\/j.robot.2026.105648_b16","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","article-title":"Applying \u201dDesign by Contract\u201d","volume":"25","author":"Meyer","year":"1992","journal-title":"Computer"},{"key":"10.1016\/j.robot.2026.105648_b17","series-title":"An Introduction to Practical Formal Methods Using Temporal Logic","author":"Fisher","year":"2011"},{"key":"10.1016\/j.robot.2026.105648_b18","series-title":"Proc. Second Workshop on Formal Methods for Autonomous Systems","first-page":"15","article-title":"Towards compositional verification for modular robotic systems","volume":"vol. 329","author":"Cardoso","year":"2020"},{"key":"10.1016\/j.robot.2026.105648_b19","series-title":"Proc. NASA Formal Methods","first-page":"353","article-title":"Heterogeneous verification of an autonomous curiosity rover","volume":"vol. 12229","author":"Cardoso","year":"2020"},{"key":"10.1016\/j.robot.2026.105648_b20","series-title":"International Conference on Space Mission Challenges for Information Technology","first-page":"15","article-title":"Early design exploration of space system scenarios using assume-guarantee contracts","author":"Rouquette","year":"2023"},{"key":"10.1016\/j.robot.2026.105648_b21","series-title":"Proceedings. 26th International Conference on Software Engineering","first-page":"221","article-title":"Compositional verification of middleware-based software architecture descriptions","author":"Caporuscio","year":"2004"},{"key":"10.1016\/j.robot.2026.105648_b22","series-title":"Contracts for Systems Design","first-page":"64","author":"Benveniste","year":"2012"},{"key":"10.1016\/j.robot.2026.105648_b23","series-title":"International Conference on Formal Methods and Models for System Design","first-page":"5","article-title":"Stochastic contracts for cyber-physical system design under probabilistic requirements","author":"Li","year":"2017"},{"key":"10.1016\/j.robot.2026.105648_b24","series-title":"International Conference on Automated Software Engineering","first-page":"702","article-title":"OCRA: A tool for checking the refinement of temporal contracts","author":"Cimatti","year":"2013"},{"key":"10.1016\/j.robot.2026.105648_b25","series-title":"NASA Formal Methods Symposium","first-page":"126","article-title":"Compositional verification of architectural models","volume":"vol. 7226","author":"Cofer","year":"2012"},{"key":"10.1016\/j.robot.2026.105648_b26","series-title":"Software Engineering and Formal Methods","first-page":"347","article-title":"CoCoSpec: A mode-aware contract language for reactive systems","volume":"vol. 9763","author":"Champion","year":"2016"},{"key":"10.1016\/j.robot.2026.105648_b27","series-title":"Proc. Computer Aided Verification","first-page":"510","article-title":"The kind 2 model checker","volume":"vol. 9780","author":"Champion","year":"2016"},{"key":"10.1016\/j.robot.2026.105648_b28","series-title":"NASA Formal Methods Symposium","first-page":"53","article-title":"Integrating formal verification and assurance: An inspection rover case study","volume":"vol. 12673","author":"Bourbouh","year":"2021"},{"issue":"2","key":"10.1016\/j.robot.2026.105648_b29","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/s10270-017-0619-4","article-title":"A Logical Approach to Systems Engineering Artifacts: Semantic Relationships and Dependencies beyond Traceability \u2013 from requirements to functional and architectural views","volume":"17","author":"Broy","year":"2018","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.robot.2026.105648_b30","series-title":"Formal Methods","first-page":"165","article-title":"IPL: An integration property language for multi-model cyber-physical systems","volume":"vol. 10951","author":"Ruchkin","year":"2018"},{"issue":"2","key":"10.1016\/j.robot.2026.105648_b31","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1109\/TSE.2010.39","article-title":"Loupe: Verifying publish-subscribe architectures with a magnifying lens","volume":"37","author":"Baresi","year":"2010","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10.1016\/j.robot.2026.105648_b32","series-title":"ECAI 2008 - 18th European Conference on Artificial Intelligence, Patras, Greece, July 21-25, 2008, Proceedings","first-page":"631","article-title":"Incremental component-based construction and verification of a robotic system","volume":"vol. 178","author":"Basu","year":"2008"},{"issue":"5s","key":"10.1016\/j.robot.2026.105648_b33","doi-asserted-by":"crossref","DOI":"10.1145\/3358197","article-title":"Compositional design of multi-robot systems control software on ROS","volume":"18","author":"Spellini","year":"2019","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"10.1016\/j.robot.2026.105648_b34","series-title":"Proc. 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","first-page":"103","article-title":"Programming safe robotics systems: Challenges and advances","volume":"vol. 11245","author":"Desai","year":"2018"},{"key":"10.1016\/j.robot.2026.105648_b35","first-page":"120","article-title":"Rule-based dynamic safety monitoring for mobile robots","volume":"7","author":"Adam","year":"2016","journal-title":"J. Softw. Eng. Robot."},{"key":"10.1016\/j.robot.2026.105648_b36","series-title":"Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering: Companion Proceedings","first-page":"5","article-title":"PROMISE: High-level mission specification for multiple robots","author":"Garc\u00eda","year":"2020"},{"key":"10.1016\/j.robot.2026.105648_b37","series-title":"2020 IEEE\/RSJ International Conference on Intelligent Robots and Systems","first-page":"7249","article-title":"Verification of system-wide safety properties of ROS applications","author":"Carvalho","year":"2020"},{"key":"10.1016\/j.robot.2026.105648_b38","series-title":"Proc. 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering","first-page":"373","article-title":"Lightweight specification and analysis of dynamic systems with rich configurations","author":"Macedo","year":"2016"},{"key":"10.1016\/j.robot.2026.105648_b39","series-title":"2016 IEEE\/RSJ International Conference on Intelligent Robots and Systems","first-page":"4491","article-title":"A framework for quality assessment of ROS repositories","author":"Santos","year":"2016"},{"key":"10.1016\/j.robot.2026.105648_b40","series-title":"2019 49th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks","first-page":"138","article-title":"SOTER: A runtime assurance framework for programming safe robotics systems","author":"Desai","year":"2019"},{"key":"10.1016\/j.robot.2026.105648_b41","series-title":"2023 IEEE International Conference on Robotics and Automation","article-title":"RoboSC: a domain-specific language for supervisory controller synthesis of ROS applications","author":"Wesselink","year":"2023"},{"issue":"5","key":"10.1016\/j.robot.2026.105648_b42","doi-asserted-by":"crossref","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","article-title":"RoboChart: Modelling and verification of the functional behaviour of robotic applications","volume":"18","author":"Miyazawa","year":"2019","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.robot.2026.105648_b43","article-title":"Formal modelling and runtime verification of autonomous grasping for active debris removal","volume":"8","author":"Farrell","year":"2021","journal-title":"Front. Robot. AI"},{"issue":"5s","key":"10.1016\/j.robot.2026.105648_b44","doi-asserted-by":"crossref","DOI":"10.1145\/3126513","article-title":"Antlab: A multi-robot task server","volume":"16","author":"Gavran","year":"2017","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"10.1016\/j.robot.2026.105648_b45","series-title":"Logic in Computer Science: Modelling and reasoning about systems","author":"Huth","year":"2004"},{"key":"10.1016\/j.robot.2026.105648_b46","series-title":"Proceedings of the 4th Conference on Logic Programming","first-page":"168","article-title":"Guarded horn clauses","volume":"vol. 221","author":"Ueda","year":"1985"},{"key":"10.1016\/j.robot.2026.105648_b47","series-title":"Parallel Logic Programming in PARLOG - The Language and Its Implementation","author":"Gregory","year":"1987"},{"key":"10.1016\/j.robot.2026.105648_b48","series-title":"Foundations of Computer Science","first-page":"46","article-title":"The Temporal Logic of Programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/j.robot.2026.105648_b49","series-title":"Formal Methods","first-page":"23","article-title":"Automated circular assume-guarantee reasoning","volume":"vol. 9109","author":"Elkader","year":"2015"},{"key":"10.1016\/j.robot.2026.105648_b50","series-title":"Temporal Logic in Specification","first-page":"62","article-title":"Temporal logic with fixed points","volume":"vol. 398","author":"Banieqbal","year":"1987"},{"issue":"3","key":"10.1016\/j.robot.2026.105648_b51","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2506375","article-title":"Loop invariants: Analysis, classification, and examples","volume":"46","author":"Furia","year":"2014","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/j.robot.2026.105648_b52","series-title":"International Conference on Computer Aided Verification","first-page":"1","article-title":"First-order theorem proving and vampire","author":"Kov\u00e1cs","year":"2013"},{"key":"10.1016\/j.robot.2026.105648_b53","doi-asserted-by":"crossref","DOI":"10.1016\/j.cosrev.2020.100270","article-title":"A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability","volume":"37","author":"Huang","year":"2020","journal-title":"Comput. Sci. Rev."},{"key":"10.1016\/j.robot.2026.105648_b54","series-title":"Principles for the development and assurance of autonomous systems for safe use in hazardous environments","author":"Luckcuck","year":"2021"},{"key":"10.1016\/j.robot.2026.105648_b55","article-title":"Using formal methods for autonomous systems: Five recipes for formal verification","author":"Luckcuck","year":"2021","journal-title":"Proc. Inst. Mech. Eng. Part O: J. Risk Reliab."},{"key":"10.1016\/j.robot.2026.105648_b56","series-title":"Working Conference on Verified Software: Theories, Tools, and Experiments","first-page":"8","article-title":"Specification: The biggest bottleneck in formal methods and autonomy","volume":"vol. 9971","author":"Rozier","year":"2016"},{"key":"10.1016\/j.robot.2026.105648_b57","series-title":"Towards Autonomous Robotic Systems","first-page":"387","article-title":"ROSMonitoring: A runtime verification framework for ROS","volume":"vol. 12228","author":"Ferrando","year":"2020"},{"key":"10.1016\/j.robot.2026.105648_b58","series-title":"Proceedings Sixth International Workshop on Formal Methods for Autonomous Systems, FMAS@IFM 2024, Manchester, UK, 11th and 12th of November 2024","first-page":"38","article-title":"Rosmonitoring 2.0: Extending ROS runtime verification to services and ordered topics","volume":"vol. 411","author":"Saadat","year":"2024"},{"key":"10.1016\/j.robot.2026.105648_b59","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2021.102610","article-title":"RML: Theory and practice of a domain specific language for runtime verification","volume":"205","author":"Ancona","year":"2021","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"10.1016\/j.robot.2026.105648_b60","doi-asserted-by":"crossref","DOI":"10.3390\/robotics10030086","article-title":"Simulating ionising radiation in gazebo for robotic nuclear inspection challenges","volume":"10","author":"Wright","year":"2021","journal-title":"Robotics"},{"key":"10.1016\/j.robot.2026.105648_b61","series-title":"Gwendolen Semantics: 2017","author":"Dennis","year":"2017"},{"key":"10.1016\/j.robot.2026.105648_b62","series-title":"2015 IEEE International Conference on Robotics and Automation","first-page":"4589","article-title":"Duality-based verification techniques for 2D SLAM","author":"Carlone","year":"2015"},{"key":"10.1016\/j.robot.2026.105648_b63","series-title":"2015 IEEE\/RSJ International Conference on Intelligent Robots and Systems","first-page":"125","article-title":"Lagrangian duality in 3D SLAM: Verification techniques and optimal solutions","author":"Carlone","year":"2015"},{"key":"10.1016\/j.robot.2026.105648_b64","series-title":"2016 IEEE\/RSJ International Conference on Intelligent Robots and Systems","first-page":"4630","article-title":"Fast global optimality verification in 3D SLAM","author":"Briales","year":"2016"},{"issue":"3","key":"10.1016\/j.robot.2026.105648_b65","first-page":"253","article-title":"Experimental verification of path planning with SLAM","volume":"5","author":"Hasegawa","year":"2016","journal-title":"IEEJ J. Ind. Appl."},{"key":"10.1016\/j.robot.2026.105648_b66","article-title":"Verification of SLAM methods implemented in ROS","volume":"6","author":"Ducho\u0148","year":"2019","journal-title":"J. Multidiscip. Eng. Sci. Technol. (JMEST)"},{"key":"10.1016\/j.robot.2026.105648_b67","doi-asserted-by":"crossref","first-page":"59","DOI":"10.22223\/tr.2016-1\/2011","article-title":"Verification of SLAM methods on ROS platform","volume":"62","author":"Siv\u1ef3","year":"2016","journal-title":"Trans. the V\u0160B-Technical Univ. Ostrav. Mech. Ser."},{"issue":"1","key":"10.1016\/j.robot.2026.105648_b68","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","article-title":"Model checking agent programming languages","volume":"19","author":"Dennis","year":"2012","journal-title":"Autom. Softw. Eng."},{"issue":"24","key":"10.1016\/j.robot.2026.105648_b69","doi-asserted-by":"crossref","DOI":"10.21105\/joss.00617","article-title":"The MCAPL framework including the agent infrastructure layer and agent java pathfinder","volume":"3","author":"Dennis","year":"2018","journal-title":"J. Open Source Software"},{"issue":"2","key":"10.1016\/j.robot.2026.105648_b70","first-page":"3","article-title":"Model Checking Programs","volume":"10","author":"Visser","year":"2002","journal-title":"Autom. Softw. Eng."},{"key":"10.1016\/j.robot.2026.105648_b71","series-title":"International Conference on Multi-Agent Systems","first-page":"312","article-title":"BDI Agents: From Theory to Practice","author":"Rao","year":"1995"},{"key":"10.1016\/j.robot.2026.105648_b72","series-title":"Verifiable Autonomous Systems: Using Rational Agents to Provide Assurance about Decisions Made by Machines","author":"Dennis","year":"2023"},{"issue":"10","key":"10.1016\/j.robot.2026.105648_b73","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Comms. the ACM"},{"key":"10.1016\/j.robot.2026.105648_b74","series-title":"Logic for Programming Artificial Intelligence and Reasoning","first-page":"348","article-title":"Dafny: An automatic program verifier for functional correctness","volume":"vol. 6355","author":"Leino","year":"2010"},{"key":"10.1016\/j.robot.2026.105648_b75","series-title":"Formal Methods for Components and Objects","first-page":"364","article-title":"Boogie: A Modular Reusable Verifier for Object-Oriented Programs","volume":"vol. 4111","author":"Barnett","year":"2005"},{"key":"10.1016\/j.robot.2026.105648_b76","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"337","article-title":"Z3: An efficient SMT solver","volume":"vol. 4963","author":"De Moura","year":"2008"},{"key":"10.1016\/j.robot.2026.105648_b77","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"331","article-title":"Learning Assumptions for Compositional Verification","volume":"vol. 2619","author":"Cobleigh","year":"2003"}],"container-title":["Robotics and Autonomous Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0921889026003209?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0921889026003209?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T03:05:55Z","timestamp":1791342355000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0921889026003209"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,11]]},"references-count":77,"alternative-id":["S0921889026003209"],"URL":"https:\/\/doi.org\/10.1016\/j.robot.2026.105648","relation":{},"ISSN":["0921-8890"],"issn-type":[{"value":"0921-8890","type":"print"}],"subject":[],"published":{"date-parts":[[2026,11]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A compositional approach to verifying modular robotic systems","name":"articletitle","label":"Article Title"},{"value":"Robotics and Autonomous Systems","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.robot.2026.105648","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"105648"}}