Publication: Verification of OpenDP Transformations
Loading...
Open/View Files
Date
2026-06-02
Authors
Published Version
Published Version
Journal Title
Journal ISSN
Volume Title
Publisher
The Harvard community has made this article openly available. Please share how this access benefits you.
Citation
Feng, Amy. 2026. Verification of OpenDP Transformations. Bachelors Thesis, Harvard University Engineering and Applied Sciences.
Abstract
Differential privacy (DP) is a method of releasing statistical information about a dataset while concealing the properties of individual data records. OpenDP is an open-source repository that allows an individual or organization to easily apply differential privacy to their statistical releases. OpenDP's transformations are a key part of manipulating datasets while ensuring differential privacy properties. Because OpenDP is used on potentially sensitive datasets, it is important to ensure that the OpenDP code is completely sound. As a first step toward formal verification of the OpenDP code, we translate the pseudocode for OpenDP functions into Lean and prove their correctness.
Description
Other Available Sources
Research Data
Keywords
Computer science
Terms of Use
This article is made available under the terms and conditions applicable to Other Posted Material (LAA), as set forth at Terms of Service