Expressing and verifying probabilistic assertions
- 5 June 2014
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 49 (6), 112-122
- https://doi.org/10.1145/2666356.2594294
Abstract
Traditional assertions express correctness properties that must hold on every program execution. However, many applications have probabilistic outcomes and consequently their correctness properties are also probabilistic (e.g., they identify faces in images, consume sensor data, or run on unreliable hardware). Traditional assertions do not capture these correctness properties. This paper proposes that programmers express probabilistic correctness properties with probabilistic assertions and describes a new probabilistic evaluation approach to efficiently verify these assertions. Probabilistic assertions are Boolean expressions that express the probability that a property will be true in a given execution rather than asserting that the property must always be true. Given either specific inputs or distributions on the input space, probabilistic evaluation verifies probabilistic assertions by first performing distribution extraction to represent the program as a Bayesian network. Probabilistic evaluation then uses statistical properties to simplify this representation to efficiently compute assertion probabilities directly or with sampling. Our approach is a mix of both static and dynamic analysis: distribution extraction statically builds and optimizes the Bayesian network representation and sampling dynamically interprets this representation. We implement our approach in a tool called Mayhap for C and C++ programs. We evaluate expressiveness, correctness, and performance of Mayhap on programs that use sensors, perform approximate computation, and obfuscate data for privacy. Our case studies demonstrate that probabilistic assertions describe useful correctness properties and that Mayhap efficiently verifies them.Keywords
Funding Information
- MARCO
- Defense Advanced Research Projects Agency
- Qualcomm
This publication has 25 references indexed in Scilit:
- Expressing and verifying probabilistic assertionsPublished by Association for Computing Machinery (ACM) ,2014
- Static analysis for probabilistic programsPublished by Association for Computing Machinery (ACM) ,2013
- Architecture support for disciplined approximate programmingPublished by Association for Computing Machinery (ACM) ,2012
- Managing performance vs. accuracy trade-offs with loop perforationPublished by Association for Computing Machinery (ACM) ,2011
- Statistical Model Checking: An OverviewLecture Notes in Computer Science, 2010
- Embedded Probabilistic ProgrammingLecture Notes in Computer Science, 2009
- Statistical probabilistic model checking with a focus on time-bounded propertiesInformation and Computation, 2006
- Error Control for Probabilistic Model CheckingLecture Notes in Computer Science, 2005
- A Measure of Asymptotic Efficiency for Tests of a Hypothesis Based on the sum of ObservationsThe Annals of Mathematical Statistics, 1952
- Sequential Tests of Statistical HypothesesThe Annals of Mathematical Statistics, 1945