SHF: Small: Probabilistic Programming and Statistical Verification for Safe Autonomy

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

Autonomous systems such as drones and self-driving cars are quickly entering human-dominated fields and becoming tangible technologies that will impact the human experience. However, as these systems share space and operate among humans, safety and reliability of autonomous systems become primary concerns. An important challenge for safety and reliability in autonomous systems is coping with uncertainty. This project focuses on three important forms of uncertainty: (1) noisy data from sensors, (2) asynchrony of distributed computation, and (3) heuristic computation of decision-making software. They bring various challenges for developing and validating software modules of autonomous systems. The project investigates a design of a language for distributed autonomous systems and associated program verification techniques that treat uncertainty as a first-class citizen. The main design goal of the language is to decouple the representation of the program code from both the probabilistic models of uncertainty and underlying solvers. For this language, the project will also develop analysis techniques that are based on statistical model checking and probabilistic program analysis. The project aims to apply the key components of the approach, including language abstractions, algorithms, and solving mechanisms, to provide end-to-end safety assurance in real-world applications. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.