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

SHF：小：安全自治的概率编程和统计验证

• 批准号: 2008883
• 负责人: Sasa Misailovic
• 金额: $ 45万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-07-01 至 2024-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2008883&HistoricalAwards=false
• 关键词: SHF; Small; Probabilistic; Programming; Statistical

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.

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

项目成果

Statheros: Compiler for Efficient Low-Precision Probabilistic Programming

• DOI: 10.1109/dac18074.2021.9586276
• 发表时间: 2021-12
• 期刊: 2021 58th ACM/IEEE Design Automation Conference (DAC)
• 作者: Jacob S. Laurel;Rem Yang;Atharva Sehgal;Shubham Ugare;Sasa Misailovic

Proof transfer for fast certification of multiple approximate neural networks

• DOI: 10.1145/3527319
• 发表时间: 2022-04
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Shubham Ugare;Gagandeep Singh

AQUA: Automated Quantized Inference for Probabilistic Programs

AQUA：概率程序的自动量化推理

• DOI: 10.1007/978-3-030-88885-5_16
• 发表时间: 2021
• 期刊: 2021 in Automated Technology for Verification and Analysis
• 作者: Huang, Zixin;Dutta, Saikat;Misailovic, Sasa
• 通讯作者: Misailovic, Sasa

SixthSense: Debugging Convergence Problems in Probabilistic Programs via Program Representation Learning

SixthSense：通过程序表示学习调试概率程序中的收敛问题

• DOI: 10.1007/978-3-030-99429-7_7
• 发表时间: 2022
• 期刊: 25th International Conference on Fundamental Approaches to Software Engineering
• 作者: Dutta, Saikat;Huang, Zixin;Misailovic, Sasa
• 通讯作者: Misailovic, Sasa

FLEX: fixing flaky tests in machine learning projects by updating assertion bounds

• DOI: 10.1145/3468264.3468615
• 发表时间: 2021-08
• 期刊: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Saikat Dutta;A. Shi;Sasa Misailovic