Benchmarks and Competitions on Formal Methods for Robotics


This is a project to develop benchmark problems for research in so-called formal methods for robotics. The repositories are hosted on GitHub at

Problem Domains

Below is a summary of problem domains, each of which is the basis for particular problem instances. With such a taxonomy, we are able to provide parameterized benchmarks that can be arbitrarily scaled, randomly generated, etc. Of course, there is also support for fixed benchmarks, e.g., as proposed from specific industrial applications. Normative descriptions are given at

  1. scaling chains of integrators
  2. traffic network of Dubins cars
  3. factory cart clearing

scaling chains of integrators

Illustration of a trajctory in 3-dimensional Euclidean space.  It avoids two gray rectangles (obstacles) and reaches a green goal rectangle.

The scaling chains of integrators domain is the simplest in terms of dynamics, yet unlike the other domains, the system to be controlled can be scaled easily to arbitrarily many dimensions. While this problem is abstract in the sense that it is not modeling a specific physical system, it is well-motivated because the double-integrator is just the basic force equation \( F=ma \) of Newtonian mechanics, up to a scaling factor. Informally, this problem domain concerns controlling acceleration or a higher order derivative of a point-mass in high-dimensional spaces so as to visit goal regions and avoid obstacles.

Get details »

traffic network of Dubins cars

Illustration of 6 Kobuki mobile bases moving around a 4-connected grid of road segments. The width is 3 road segments, and the height is 2 road segments. Each has two lanes, where there is one lane for each direction of traffic.

The traffic network of Dubins cars domain involves navigation in a small network of two-lane roads with vehicles that have Dubins car dynamics. There is an adversary that selects the motion of other cars. The adversary is subject to assumptions such as obeying traffic rules and not parking unfairly at locations that must be eventually reached by the controller.

Get details »

factory cart clearing

Illustration of a Baxter robot next to an empty table.  The arms are hanging downward and not in motion.

The factory cart clearing domain concerns dexterous manipulation tasks motivated by assembly line activities. The robot is required to process objects laid out on a cart that is brought to it and sort them into bins. Carts arrive after the robot indicates that it is ready, and carts are removed once a robot declares that it is done. Scoring will be based on how many carts can be processed correctly (described below) in a fixed amount of time.


Scott C. Livingston <[email protected]>, where A =
Vasumathi Raman <[email protected]>, where B =