Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | English |
| Published: |
Zenodo
2025
|
| Online Access: | https://doi.org/10.5281/zenodo.17034603 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866902157079347200 |
|---|---|
| author | Yan, Pengbo |
| author_facet | Yan, Pengbo |
| contents | <p>Artifact for Pengbo Yan’s PhD Thesis<br>"Formally Verifying the Security of Probabilistic Oblivious Algorithms"</p> <p>Author: Pengbo Yan<br>Year: 2025</p> <p>License: 2-Clause BSD License (https://opensource.org/license/BSD-2-Clause)</p> <p>A predecessor of this artifact was published on https://zenodo.org/records/12755500</p> <p>This artifact contains the Isabelle/HOL formalization of the extended Probabilistic Separation Logic (PSL) and the transformation framework introduced in the thesis. <br>All theories have been tested with Isabelle2022/HOL on both Windows (by GUI) and macOS (by GUI and command lines).</p> <p>The formalization of transformations depends on CryptHOL’s definitions of negligible functions, available in the Archive of Formal Proofs (AFP): https://www.isa-afp.org/</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_17034603 |
| institution | Zenodo |
| language | eng |
| publishDate | 2025 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Formally Verifying the Security of Probabilistic Oblivious Algorithms Yan, Pengbo <p>Artifact for Pengbo Yan’s PhD Thesis<br>"Formally Verifying the Security of Probabilistic Oblivious Algorithms"</p> <p>Author: Pengbo Yan<br>Year: 2025</p> <p>License: 2-Clause BSD License (https://opensource.org/license/BSD-2-Clause)</p> <p>A predecessor of this artifact was published on https://zenodo.org/records/12755500</p> <p>This artifact contains the Isabelle/HOL formalization of the extended Probabilistic Separation Logic (PSL) and the transformation framework introduced in the thesis. <br>All theories have been tested with Isabelle2022/HOL on both Windows (by GUI) and macOS (by GUI and command lines).</p> <p>The formalization of transformations depends on CryptHOL’s definitions of negligible functions, available in the Archive of Formal Proofs (AFP): https://www.isa-afp.org/</p> |
| title | Formally Verifying the Security of Probabilistic Oblivious Algorithms |
| url | https://doi.org/10.5281/zenodo.17034603 |