基于 Isabelle/HOL 的混合系统微分 Hoare 逻辑与精化演算
计算机科学中的逻辑
2019-10-31 v1
摘要
我们提出了混合系统的简单新型 Hoare 逻辑与精化演算，其风格类似于微分动态逻辑。（精化）带测试的 Kleene 代数用于推理程序结构并在此层次上生成验证条件。透镜以泛型代数方式捕获混合程序存储。该方法已用 Isabelle/HOL 证明助手形式化。若干实例阐释了所得验证组件的工作流程。
引用
@article{arxiv.1910.13554,
title = {Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL},
author = {Simon Foster and Jonathan Julián Huerta y Munive and Georg Struth},
journal= {arXiv preprint arXiv:1910.13554},
year = {2019}
}
备注
13 pages, no figures, conference