3.8 Proceedings Paper

Progress in Certifying Hardware Model Checking Results

期刊

COMPUTER AIDED VERIFICATION, PT II, CAV 2021
卷 12760, 期 -, 页码 363-386

出版社

SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-030-81688-9_17

关键词

-

资金

  1. Austrian Science Fund (FWF) [W1255-N23]
  2. State of Upper Austria
  3. Academy of Finland [336092]
  4. Academy of Finland (AKA) [336092] Funding Source: Academy of Finland (AKA)

向作者/读者索取更多资源

A formal framework was presented to certify k-induction-based model checking results, utilizing the concept of k-witness circuit and a simple inductive invariant. The approach reduces the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation in order to allow proofs to be checked with an independent proof checker. The resulting certification toolkit CERTIFAIGER was evaluated on instances from the hardware model checking competition, demonstrating the practical use of the certification method.
We present a formal framework to certify k-induction-based model checking results. The key idea is the notion of a k-witness circuit which simulates the given circuit and has a simple inductive invariant serving as proof certificate. Our approach allows to check proofs with an independent proof checker by reducing the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation. We also present CERTIFAIGER, the resulting certification toolkit, and evaluate it on instances from the hardware model checking competition. Our experiments show the practical use of our certification method.

作者

我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。

评论

主要评分

3.8
评分不足

次要评分

新颖性
-
重要性
-
科学严谨性
-
评价这篇论文

推荐

暂无数据
暂无数据