Formal methods

Sharing the World with Autonomous Systems: What Goes Wrong and How to Fix It (NSF)

Develop efficient algorithms for autonomous systems to characterize and actively identify the inconsistencies (e.g., in perception and decision-making) among the interacting agents and to influence the behaviors of the other agents to improve the safety of the overall system.

CAREER: Establishing Correctness of Learning-Enabled Autonomous Systems with Conflicting Requirements (NSF)

Develop specification formalisms, control synthesis algorithms, and quantitative verification frameworks for autonomous systems that include learning-based components, operate in uncertain environments, and are subject to conflicting requirements with partially established priorities.

Resource-Aware Hierarchical Runtime Verification for Mixed-Abstraction-Level Systems of Systems (NSF)

Develop runtime verification techniques that incorporate mixed-abstraction-level granularity in specifications and enable on-deadline mitigation triggering

Planning with Conflicting Specifications

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

Formal Specifications of Autonomous Systems

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

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.

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.

DARPA Urban Challenge 2007

A race of autonomous ground vehicles through an urban environment.