Nils Froleyks, Zhengqi Yu, Armin Biere, Keijo Heljanko,
"Certifying Phase Abstraction"
, in Ch. Benzmüller, M. J.H. Heule, R. A. Schmidt: Automated Reasoning, 12th International Joint Conference, IJCAR 2024, Serie Lecture Notes in Computer Science, Vol. 14739, Springer, Seite(n) 284?303, 7-2024, ISBN: 978-3-031-63498-7
Original Titel:
Certifying Phase Abstraction
Sprache des Titels:
Englisch
Original Buchtitel:
Automated Reasoning, 12th International Joint Conference, IJCAR 2024
Original Kurzfassung:
Certification helps to increase trust in formal verification ofsafety-critical systems which require assurance on theircorrectness. In hardware model checking, a widely used formalverification technique, phase abstraction is considered one of themost commonly used preprocessing techniques. We present an approachto certify an extended form of phase abstraction using a genericcertificate format. As in earlier works our approach involvesconstructing a witness circuit with an inductive invariant propertythat certifies the correctness of the entire model checking process,which is then validated by an independent certificate checker. Wehave implemented and evaluated the proposed approach includingcertification for various preprocessing configurations on hardwaremodel checking competition benchmarks. As an improvement on previouswork in this area, the proposed method is able to efficientlycomplete certification with an overhead of a fraction of modelchecking time.
Forschungs-