Proving partial-correctness and invariance properties of transition-system models

Vlad Rusu,Gilles Grimaud,Michaël Hauspie

Science of Computer Programming（2020）

引用 7|浏览34

暂无评分

摘要

We propose an approach for proving partial-correctness and invariance properties of transition systems, and illustrate it on a model of a security hypervisor.

查看译文

关键词

Formal verification,Coinduction,Coq proof assistant,Reachability Logic,Hypervisor

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要