Certifying Phase Abstraction
arxiv(2024)
摘要
Certification helps to increase trust in formal verification of
safety-critical systems which require assurance on their correctness. In
hardware model checking, a widely used formal verification technique, phase
abstraction is considered one of the most commonly used preprocessing
techniques. We present an approach to certify an extended form of phase
abstraction using a generic certificate format. As in earlier works our
approach involves constructing a witness circuit with an inductive invariant
property that certifies the correctness of the entire model checking process,
which is then validated by an independent certificate checker. We have
implemented and evaluated the proposed approach including certification for
various preprocessing configurations on hardware model checking competition
benchmarks. As an improvement on previous work in this area, the proposed
method is able to efficiently complete certification with an overhead of a
fraction of model checking time.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要