SHF: Small: Reasoning Rigorously About Probabilistic Programs

随着社会越来越依赖软件系统来帮助制定医疗计划、预测未来气候、指导金融市场投资，以及挖掘噪声数据来推断科学事实，输入数据的不确定性和软件的缺陷可能产生错误警报或错误的安全感的风险越来越高。这个项目将有助于解决高度复杂的概率程序和推理工具之间的差距。概率程序出现在重要的日常应用中，包括医疗、工程和金融风险分析/决策系统、大规模模拟、数据挖掘、网络物理系统的传感器噪声过滤算法和随机算法。程序行为中存在的输入不确定性和随机性可能会导致不良行为和可变性能。 因此，重要的是要准确地预测这种不良行为的概率，和expectedvalues为重要的性能measure.This项目研究自动程序分析工具的概率程序，将建模的不确定性的来源适当，并推断上的断言和预期的性能measurements的概率范围。两种风格的推理程序正在研究：符号程序结合决策程序与鞅理论和统计程序使用统计假设检验方法来推断概率注释与prosticalguarantee.

As society becomes increasingly reliant on software systems to helpplan medical treatments, predict the future climate, guide investmentsin financial markets, and mine noisy data to infer scientific facts,the risk that uncertainties in the input data and defects in thesoftware can create false alarms, or a false sense of security, ishigh. This project will help address the gap between highly complexprobabilistic programs and tools for reasoning about them.Probabilistic programs arise in important everyday applications thatinclude medical, engineering and financial risk analysis/decisionmaking systems, large-scale simulations, data mining, sensor noisefiltering algorithms for cyber-physical systems, and randomizedalgorithms. The presence of input uncertainties and randomness builtinto the behavior of the programs can cause undesirable behaviors andvariable performance. Therefore, it is important to accuratelypredict the probabilities of such undesirable behaviors, and expectedvalues for important performance measures.This project investigates automatic program analysis tools forprobabilistic programs that will model the sources of uncertaintyappropriately, and infer bounds on the probabilities of assertions andexpectations of performance measures. Two flavors of inferenceprocedures are being investigated: symbolic procedurescombining decision procedures with the theory of martingales andstatistical procedures using statistical hypothesis testingmethods to infer probabilistic annotations with statisticalguarantees.