Formal verification
Related papers: 20
About
Formal verification is a mathematically rigorous approach to proving that a system behaves correctly according to a precise specification, using techniques such as model checking, theorem proving, and runtime verification. Unlike testing or simulation, which can only examine a finite set of scenarios, formal verification exhaustively analyzes all possible system states or executes monitors during operation to guarantee that certain properties always hold or never occur. In robotics and AI, formal verification is applied to ensure safety-critical behaviors in autonomous systems, multi-robot coordination, motion planning, human-robot collaboration, and robotic operating system frameworks like ROS. Tools such as timed automata and Petri nets allow engineers to model concurrent robot actions, timing constraints, and communication protocols, then automatically check whether the system satisfies requirements like collision avoidance or task completion guarantees. Formal verification matters because autonomous robots increasingly operate in unpredictable environments alongside humans, where failures can cause physical harm or mission-critical errors. By providing mathematical proof of correctness rather than empirical confidence, it strengthens trust, supports regulatory compliance, and enables safer deployment of robotic systems in healthcare, manufacturing, autonomous driving, and other high-stakes domains.
Top Researchers
Top Institutes
Top Cited Papers
Limits for automatic verification of finite-state concurrent systems
Krzysztof R. Apt, Dexter Kozen
Citations: 375 • 1986
Formal Specification and Verification of Autonomous Robotic Systems
Matt Luckcuck, Marie Farrell, Louise A. Dennis, Clare Dixon, Michael Fisher
Citations: 264 • 2019
Formal Approach to the Deployment of Distributed Robotic Teams
Yu‐Shan Chen, Xu Chu Ding, Alin Ştefănescu, Călin Belta
Citations: 140 • 2011
Multi-robot planning : a timed automata approach
Michael Melholt Quottrup, Thomas Bak
Citations: 105 • 2004
ROSRV: Runtime Verification for Robots
Jeff Huang, Cansu Erdoğan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind Sundaresan, Grigore Roşu
Citations: 97 • 2014
Combining Model Checking and Runtime Verification for Safe Robotics
Ankush Desai, Tommaso Dreossi, Sanjit A. Seshia
Citations: 75 • 2017
Cluster Tools With Chamber Revisiting—Modeling and Analysis Using Timed Petri Nets
W.M. Zuberek
Citations: 73 • 2004
“Dave...I can assure you ...that it’s going to be all right ...” A Definition, Case for, and Survey of Algorithmic Assurances in Human-Autonomy Trust Relationships
Citations: 72 • 2019
Safety Assessment of Collaborative Robotics Through Automated Formal Verification
Federico Vicentini, Mehrnoosh Askarpour, Matteo Rossi, Dino Mandrioli
Citations: 71 • 2019
Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study
Matt Webster, Clare Dixon, Michael Fisher, Maha Salem, Joe Saunders, Kheng Lee Koay, Kerstin Dautenhahn, Joan Sàez-Pons
Citations: 70 • 2015
Living with Uncertainty in the Age of Runtime Models
Holger Giese, Nelly Bencomo, Liliana Pasquale, Andres J. Ramirez, Paola Inverardi, Sebastian Wätzoldt, Siobhán Clarke
Citations: 65 • 2014
Formal verification of a TDMA protocol start-up mechanism
Henrik Lönn, Paul Pettersson
Citations: 65 • 2002
Verification of Hybrid Systems
Laurent Doyen, Goran Frehse, George J. Pappas, André Platzer
Citations: 62 • 2018
Formal methods to comply with rules of the road in autonomous driving: State of the art and grand challenges
Noushin Mehdipour, Matthias Althoff, Radboud Duintjer Tebbens, Călin Belta
Citations: 62 • 2023
Runtime Verification of Component-Based Systems
Ylìès Falcone, Mohamad Jaber, Thanh-Hung Nguyen, Marius Bozga, Saddek Bensalem
Citations: 57 • 2011
Formal Verification of ROS-Based Robotic Applications Using Timed-Automata
Raju Halder, José Proença, Nuno Macedo, André Santos
Citations: 57 • 2017
A corroborative approach to verification and validation of human–robot teams
Citations: 52 • 2019
ROSMonitoring: A Runtime Verification Framework for ROS
Angelo Ferrando, Rafael C. Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini, Viviana Mascardi
Citations: 49 • 2020
A Formal Model-Based Design Method for Robotic Systems
Rui Wang, Yong Guan, Houbing Song, Xinxin Li, Xiaojuan Li, Zhiping Shi, Xiaoyu Song
Citations: 47 • 2018
Towards automatic verification of autonomous systems
Reid Simmons, Charles Pecheur, Grama R. Srinivasan
Citations: 45 • 2002