Emily Zhengqi Yu,
"Certifying hardware model checking"
, Johannes Kepler Universität Linz, 7-2023
Original Titel:
Certifying hardware model checking
Sprache des Titels:
Englisch
Original Kurzfassung:
Ensuring the correctness of safety-critical systems is of paramount importance, and it is becoming increasingly vital to utilize formal verification techniques to achieve this. In automated reasoning for formal verification, verifiers generate certificates in the form of machine checkable proofs, in addition to providing simply a yes or no verification result. These certificates are then validated independently by formally verified tools, and can be be subject to an additional layer of verification by trusted theorem provers. The research endeavors in this thesis are focused on the domain of hardware model checking.
This thesis introduces a novel certificate format that is highly adaptable for various model checking techniques. The novel witness circuit certificate contains an inductive invariant and can be readily verified via simple SAT checks. The framework initially involved a one-alternation QBF check for the witness circuit, but through further study and experimentation, we were able to eliminate the quantifiers and simplify the certification process to pure SAT checks. The certificate format was further refined to enable more advanced preprocessing model checking techniques, such as phase abstraction and cone-of-influence reduction, to be incorporated.
The certification framework proposed covers a range of model checking techniques, including the well-established temporal induction (also known as k-induction). This research also contributes by providing a concrete construction of a certificate specifically for this technique, effectively utilizing the certificate format. Additionally, to demonstrate the versatility of our approach, the scope is expanded from bit-level to word-level model checking by leveraging quantifier-free fixed-size bit-vectors.
Furthermore, the framework extends to certifying preprocessing techniques for model checking. The certificate format is effectively applied to temporal decomposition, enabling the generation of a single witness circuit for the entire model checking process, including both preprocessing and base model checking. In addition, this thesis addresses another popular and important preprocessing technique namely phase abstraction. Notably, the proposed certification approach is complete, such that whenever model checking is successful, a valid certificate can be produced.
The certification framework has been implemented in the tool suite, CERTIFAIGER, along with its extensions, rigorously evaluated through empirical experiments, demonstrating the effectiveness and practicality of the methodology. While not a primary focus of the research, it is worth noting that our work has yielded valuable benchmarks that can be of use to both the QBF and SAT communities.
Forschungs-