Verse

Python multi-agent verification library

Verse is a Python library for creating, simulating, and verifying scenarios with interacting, decision making agents. The decision logic of an agent can be written in an expressive subset of Python. The continuous evolution can be described as a black-box function. The agent can be ported across different maps, which can be defined from scratch or imported from opendrive files. Verse scenarios can be simulated and verified using hybrid reachability analysis algorithms. The initial implementation of reachability analysis used intervals (hyperrectangles) as the main data structure.

Website   Code   Funding: NASA

GRAIC

Autonomous racing controller and evaluation framework

GRAIC is built on CARLA and provides a simulation environment, test vehicles, tracks, and scoring function for autonomous vehicle racing controllers. The cars have to go through waypoints or gates and avoid other cars. It was used for several competitions in the past and is now routinely used by students int he Safe Autonomy (ECE484) course at Illinois.

Website   Code    Funding: NSA

FACTEST

Controller synthesis for reach-avoid specifications

FACTEST is tool for synthesizing controllers for nonlinear systems with reach-avoid requirements. The controllers found by FACTEST consists of a reference trajectory and a tracking controller which drives the actual trajectory to follow the reference trajectory. It has been used to find trajectories and control signals for ground and air vehicle models in maze-like environments.

Website   Code    Funding: NASA, AFOSR

NeuReach

Neural reachability

NeuReach is a tool that uses neural networks to represent and compute reachable sets from executions of a dynamical systems.

Website   Code    Funding: NSF

CyPhyHouse and Koord

Programming language and runtime system for distributed robotics

CyPhyHouse and the Koord programming language aid development, debugging, and deployment of distributed mobile robotic applications using a shared memory-like abstraction. This toolbox helps develop hardware-agnostic, distributed applications using the high-level, event driven Koord programming language. CyPhyHouse is designed with the aim of porting higer-level applications across hardware platforms without requiring expertise in controller design or distributed network protocols.

Website   Code    Funding: NSF CPS