As society becomes increasingly reliant on software systems to help plan medical treatments, predict the future climate, guide investments in financial markets, and mine noisy data to infer scientific facts, the risk that uncertainties in the input data and defects in the software can create false alarms, or a false sense of security, is high. This project will help address the gap between highly complex probabilistic programs and tools for reasoning about them. Probabilistic programs arise in important everyday applications that include medical, engineering and financial risk analysis/decision making systems, large-scale simulations, data mining, sensor noise filtering algorithms for cyber-physical systems, and randomized algorithms. The presence of input uncertainties and randomness built into the behavior of the programs can cause undesirable behaviors and variable performance. Therefore, it is important to accurately predict the probabilities of such undesirable behaviors, and expected values for important performance measures.
This project investigates automatic program analysis tools for probabilistic programs that will model the sources of uncertainty appropriately, and infer bounds on the probabilities of assertions and expectations of performance measures. Two flavors of inference procedures are being investigated: symbolic procedures combining decision procedures with the theory of martingales and statistical procedures using statistical hypothesis testing methods to infer probabilistic annotations with statistical guarantees.
