ZK-ProVer: Non-Interactive Zero-Knowledge Certification for SAT-Based Program Verification
Guoqiang Li
Program verification ensures software correctness through formal methods but often incurs substantial computational overhead. In SAT-based verification, the verification task is reduced to satisfiability checking, where satisfiable instances yield concrete counterexamples and unsatisfiable instances are certified by resolution proofs. While satisfying assignments and resolution proofs are useful for establishing correctness, they may expose defect-relevant details, including concrete inputs that