期刊
COMPUTER AIDED VERIFICATION, PT II, CAV 2021
卷 12760, 期 -, 页码 363-386出版社
SPRINGER INTERNATIONAL PUBLISHING AG
DOI: 10.1007/978-3-030-81688-9_17
关键词
-
类别
资金
- Austrian Science Fund (FWF) [W1255-N23]
- State of Upper Austria
- Academy of Finland [336092]
- 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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据