Formal methods

DARPA Urban Challenge 2007

A race of autonomous ground vehicles through an urban environment.

Formal Methods for Design and Verification of Embedded Control Systems

Develop mathematical and computational frameworks to facilitate the design and analysis of embedded control systems such as autonomous vehicles.

Formal Specifications of Autonomous Systems

Derive, analyze, and refine specifications from regulatory requirements and demonstrations.

Planning with Conflicting Specifications

Develop planning and decision-making algorithms with multiple, potentially conflicting objectives.

Temporal Logic Planning (TuLiP) Toolbox

A Python-based software toolbox for the synthesis of embedded control software that is provably correct with respect to an expressive subset of linear temporal logic (LTL) specifications.