Stratified Certification for k-Induction

TL;DR

This paper introduces a simplified, efficient stratified certification method for k-induction model checking that improves performance and extends to word-level verification, making certification more practical and scalable.

Contribution

It proposes a stratified approach that reduces complexity and enhances efficiency in k-induction certification, enabling word-level verification with fewer SAT checks.

Findings

Substantial performance improvements demonstrated in experiments.

Certification remains in co-NP complexity class.

Successful implementation of the Certifaiger-wl tool for word-level model checking.

Abstract

Our recently proposed certification framework for bit-level k-induction-based model checking has been shown to be quite effective in increasing the trust of verification results even though it partially involved quantifier reasoning. In this paper we show how to simplify the approach by assuming reset functions to be stratified. This way it can be lifted to word-level and in principle to other theories where quantifier reasoning is difficult. Our new method requires six simple SAT checks and one polynomial-time check, allowing certification to remain in co-NP while the previous approach required five SAT checks and one QBF check. Experimental results show a substantial performance gain for our new approach. Finally, we present and evaluate our new tool Certifaiger-wl which is able to certify k-induction-based word-level model checking.