KIV: overview and VerifyThis competition
KIV: overview and VerifyThis competition
复制标题
DOI：
10.1007/s10009-014-0308-3
复制
发表时间：
2015-11-01
影响因子：
1.5
通讯作者：
Reif, Wolfgang
中科院分区：
文献类型：
--
作者：
Ernst, Gidon;Pfaehler, Joerg;Reif, Wolfgang
我们的研究小组的成员使用互动规范和验证系统KIV参加了2012年FM 2012上的验证竞赛。在本文中，我们描述了KIV验证系统及其最新添加。我们讨论了三个验证问题的解决方案，以及KIV的哪些特征用于解决这些问题。我们还报告了执行证明的发现。
Members of our research group participated in the VerifyThis competition at FM 2012 in Paris using the interactive specification and verification system KIV. In this article we describe the KIV verification system and its latest additions. We discuss our solutions to the three VerifyThis problems and which features of KIV were used in solving them. We also report on our findings from performing the proofs.