On Tuesday, June 2, Arman Ferdowsi gave a talk at the Formal Methods in Systems Engineering group (FORSYTE)↗ at the Technische Universität Wien↗. The talk was part of the RiSE seminar and VCLA talks series. You can find more information on the series and other talks on the FORSYTE website↗.
Title: Beyond Time-to-Answer: Certificate-Aware PDR for Trustworthy Hardware Model Checking
Abstract: Property-Directed Reachability, also known as PDR/IC3, is one of the standard techniques for proving safety properties of hardware systems. Traditionally, PDR implementations are optimized mainly for finding an answer quickly, while the produced invariant or counterexample is treated as a secondary artifact. In certified verification workflows, however, this artifact becomes part of the deliverable: it must be independently checked, stored, reproduced, and validated.
This talk presents CAPDR, a Certificate-Aware variant of PDR that makes certificate quality a first-class objective. CAPDR jointly targets solving time, certificate size, independent checker time, and reproducibility. Its key idea is to use a learned ranking policy only to guide selected PDR choice points, such as blocker generalization, obligation ordering, and clause pushing. Soundness is preserved because every state-changing step remains protected by the standard SAT-based PDR checks, and a SAFE or UNSAFE result is reported only after an independent checker accepts the emitted invariant or counterexample trace.
Overall, the talk shows how certificate-aware search can make PDR not only effective at proving safety, but also better suited for certified workflows by producing smaller, faster-checking, and more reproducible verification artifacts.