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!
|
Table of 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>