Model checking

Model checking for programming languages using VeriSoft

Patrice Godefroid

Citations: 828 • 1997

Model checking JAVA programs using JAVA PathFinder

Klaus Havelund, Thomas Pressburger

Citations: 798 • 2000

Temporal logic motion planning for dynamic robots

Georgios Fainekos, Antoine Girard, Hadas Kress‐Gazit, George J. Pappas

Citations: 460 • 2008

HyTech: A model checker for hybrid systems

Thomas A. Henzinger, Pei-Hsin Ho, Howard Wong-Toi

Citations: 421 • 1997

Limits for automatic verification of finite-state concurrent systems

Krzysztof R. Apt, Dexter Kozen

Citations: 375 • 1986

MCMAS: A Model Checker for the Verification of Multi-Agent Systems

Alessio Lomuscio, Hongyang Qu, Franco Raimondi

Citations: 290 • 2009

Temporal Logic Motion Planning for Mobile Robots

Georgios Fainekos, Hadas Kress‐Gazit, George J. Pappas

Citations: 233 • 2006

Automatic Deployment of Distributed Teams of Robots From Temporal Logic Motion Specifications

Marius Kloetzer, Călin Belta

Citations: 179 • 2009

Formal analysis of a space-craft controller using SPIN

Klaus Havelund, M. Lowry, John Penix

Citations: 178 • 2001

Hybrid Controllers for Path Planning: A Temporal Logic Approach

Georgios Fainekos, Hadas Kress‐Gazit, George J. Pappas

Citations: 172 • 2006

Temporal Logic Motion Planning and Control With Probabilistic Satisfaction Guarantees

Morteza Lahijanian, Sean B. Andersson, Călin Belta

Citations: 148 • 2011

Formal Approach to the Deployment of Distributed Robotic Teams

Yu‐Shan Chen, Xu Chu Ding, Alin Ştefănescu, Călin Belta

Citations: 140 • 2011

Exact Collision Checking of Robot Paths

Fabian Schwarzer, Mitul Saha, Jean‐Claude Latombe

Citations: 121 • 2004

RoboChart: modelling and verification of the functional behaviour of robotic applications

Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, Jon Timmis, Jim Woodcock

Citations: 113 • 2019

Multi-robot planning : a timed automata approach

Michael Melholt Quottrup, Thomas Bak

Citations: 105 • 2004

Revising motion planning under Linear Temporal Logic specifications in partially known workspaces

Meng Guo, Karl Henrik Johansson, Dimos V. Dimarogonas

Citations: 104 • 2013

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

PRISM-games 3.0: Stochastic Game Verification with Concurrency, Equilibria and Time

Marta Kwiatkowska, Gethin Norman, David Parker, Gabriel Santos

Citations: 66 • 2020

Formal verification of a TDMA protocol start-up mechanism

Henrik Lönn, Paul Pettersson

Citations: 65 • 2002