ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification 事件

ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification arXiv:2605.27051v1 Announce Type: cross Abstract: Formal verification of large C programs is impeded by state-space explosion: Bounded Model Checking (BMC) tools must encode the entire state space up to the predetermined bound by unrolling all nested constructs. We present ConVer, a top-down compositional verification tool. Given a C program with a top-level assertion, ConVer decomposes verification t