Verifying Probabilistic Programs in Rust
a day ago
- #probabilistic-verification
- #formal-methods
- #rust-programming
- 现有的概率程序验证工具局限于理想化语言，而非实际生产代码。
- Alerus 是一个验证概率性 Rust 程序的新框架，它通过概率推理扩展了 Verus 工具的功能。
- 它利用轻量级概率误差信用（幽灵状态）来验证随机抽样算法的正确性。
- 多个离散分布的抽样例程已通过 Alerus 得到验证。
- 通过将 Verus 的逻辑模型与 Eris 的概率最弱前置条件相结合，并在 Rocq 中机械化实现，建立了该框架的可靠性。