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

无人机和自动驾驶汽车等自动驾驶系统正在迅速进入人类主导的领域，并成为影响人类体验的有形技术。然而，由于这些系统共享空间并在人类之间运行，因此自主系统的安全性和可靠性成为主要问题。自主系统安全性和可靠性的一个重要挑战是应对不确定性。该项目主要关注三种重要形式的不确定性：（1）来自传感器的噪声数据，（2）分布式计算的复杂性，以及（3）决策软件的启发式计算。他们带来了开发和验证自治systems.The项目的软件模块的各种挑战研究的分布式自治系统和相关的程序验证技术，把不确定性作为一等公民的语言的设计。该语言的主要设计目标是将程序代码的表示与不确定性的概率模型和底层求解器解耦。对于这种语言，该项目还将开发基于统计模型检查和概率程序分析的分析技术。该项目旨在应用该方法的关键组成部分，包括语言抽象、算法和解决机制，在现实世界的应用中提供端到端的安全保证。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.