Model checking has emerged as a crucial formal verification technique for ensuring the correctness of safety-critical systems. Among its various approaches, the IC3 algorithm represents an important advancement in symbolic model checking, but its efficiency is limited by the computational cost of constraint solver invocations during clause generalization phases, where each generalization process typically yields only a single inductive clause despite the substantial solving effort required. We present a new approach that improves how IC3 explores invariant spaces through batch clause construction and incremental solving. Traditional IC3 implementations sequentially test literals for removal, requiring multiple expensive solver calls yet producing only a single generalized clause per iteration. Our framework introduces an alternative approach: instead of focusing on which literals to remove, we construct and verify multiple potential generalization candidates simultaneously. This combinatorial verification methodology enables the discovery of multiple inductive clauses from a single counterexample, expanding the invariant space covered in each solver invocation. Our approach examines intermediate results from verification steps and reuses this information to derive multiple valid clause generalizations in a single solver invocation. This methodology constrains the search space of the verification problem and influences the verification path, yielding more compact and precise invariants that improve the overall verification process. Through formal analysis, we establish the soundness of our approach and show how it enhances abstract state representation. Experimental evaluation across 1349 benchmarks from the FMCAD08 suite shows our method (BCCIC3) achieves a 21.21% reduction in overall verification time compared to state-of-the-art IC3 implementations. The techniques presented advance property-directed reachability algorithms with applications in hardware verification, software model checking, and cyber-physical system verification.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

BCCIC3: Batch Clause Construction Enhanced Generalization in IC3

  • Yi Chen,
  • Xinyi Gong,
  • Liangze Yin,
  • Ji Wang,
  • Ting Wang

摘要

Model checking has emerged as a crucial formal verification technique for ensuring the correctness of safety-critical systems. Among its various approaches, the IC3 algorithm represents an important advancement in symbolic model checking, but its efficiency is limited by the computational cost of constraint solver invocations during clause generalization phases, where each generalization process typically yields only a single inductive clause despite the substantial solving effort required. We present a new approach that improves how IC3 explores invariant spaces through batch clause construction and incremental solving. Traditional IC3 implementations sequentially test literals for removal, requiring multiple expensive solver calls yet producing only a single generalized clause per iteration. Our framework introduces an alternative approach: instead of focusing on which literals to remove, we construct and verify multiple potential generalization candidates simultaneously. This combinatorial verification methodology enables the discovery of multiple inductive clauses from a single counterexample, expanding the invariant space covered in each solver invocation. Our approach examines intermediate results from verification steps and reuses this information to derive multiple valid clause generalizations in a single solver invocation. This methodology constrains the search space of the verification problem and influences the verification path, yielding more compact and precise invariants that improve the overall verification process. Through formal analysis, we establish the soundness of our approach and show how it enhances abstract state representation. Experimental evaluation across 1349 benchmarks from the FMCAD08 suite shows our method (BCCIC3) achieves a 21.21% reduction in overall verification time compared to state-of-the-art IC3 implementations. The techniques presented advance property-directed reachability algorithms with applications in hardware verification, software model checking, and cyber-physical system verification.