NDLI: Expressing and verifying probabilistic assertions

Content Provider	ACM Digital Library
Author	Panchekha, Pavel Grossman, Dan McKinley, Kathryn S. Ceze, Luis Sampson, Adrian Mytkowicz, Todd
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.
Starting Page	112
Ending Page	122
Page Count	11
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2666356.2594294
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	49
Issue Number	6
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Differential privacy Data obfuscation Approximate computing Probabilistic programming Sensors Symbolic execution
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Expressing and verifying probabilistic assertions

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Assertions in programming languages

Directed incremental symbolic execution

Compositional solution space quantification for probabilistic software analysis

Verifying systems rules using rule-directed symbolic execution (SIGP, Vol. 48, Issue. 4)

Verifying quantitative reliability for programs that execute on unreliable hardware

Probability type inference for flexible approximate programming

Probabilistic relational reasoning for differential privacy

Expressing and verifying probabilistic assertions

Similar Documents

Expressing and verifying probabilistic assertions

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Assertions in programming languages

Directed incremental symbolic execution

Compositional solution space quantification for probabilistic software analysis

Verifying systems rules using rule-directed symbolic execution (SIGP, Vol. 48, Issue. 4)

Verifying quantitative reliability for programs that execute on unreliable hardware

Probability type inference for flexible approximate programming

Probabilistic relational reasoning for differential privacy

Expressing and verifying probabilistic assertions