Global guidance for local generalization in model checking

Area of Science:

• Formal methods
• Computer science
• Software engineering

Background:

• SMT-based model checkers, particularly IC3-style algorithms, are leading techniques for verifying infinite state systems.
• These methods infer global inductive invariants using local reasoning on transition relations, enhanced by SMT procedures like interpolation.
• However, reliance on SMT solver heuristics can compromise model checking stability.

Purpose of the Study:

• To systematically address the limitations of local reasoning in SMT-based model checking.
• To introduce explicit global guidance into the local reasoning of IC3-style algorithms.
• To improve the stability and effectiveness of infinite state system verification.

Main Methods:

• Extension of the SMT-IC3 paradigm with three novel rules for global guidance.
• Instantiation of these rules for Linear Integer Arithmetic and Linear Rational Arithmetic.
• Implementation of the enhanced algorithm, GSpacer, on top of the Spacer solver within Z3.

Main Results:

• GSpacer demonstrates significantly improved effectiveness compared to the original Spacer algorithm.
• The enhanced method also surpasses the performance of solely global reasoning approaches.
• GSpacer exhibits insensitivity to interpolation, a common factor affecting SMT solver performance.

Conclusions:

• Explicit global guidance is a systematic and effective way to overcome locality limitations in SMT-based model checking.
• GSpacer offers a more robust and efficient solution for verifying infinite state systems.
• The proposed method enhances verification stability and performance by reducing reliance on SMT solver-specific heuristics.