在Isabelle中使用pGCL验证概率正确性
计算机科学中的逻辑
2012-11-28 v1 编程语言
摘要
本文介绍了在Isabelle/HOL中pGCL的形式化。使用浅嵌入，我们展示了与现有自动化支持的紧密集成。我们展示了该模型可以轻松扩展以纳入现有结果，包括L4.verified项目的结果。我们激励了该形式化在机械验证概率安全属性方面的适用性，包括真实系统中侧信道对策的有效性。
关键词
引用
@article{arxiv.1211.6197,
title = {Verifying Probabilistic Correctness in Isabelle with pGCL},
author = {David Cock},
journal= {arXiv preprint arXiv:1211.6197},
year = {2012}
}
备注
In Proceedings SSV 2012, arXiv:1211.5873