Completeness Thresholds in Bounded Model Checking

Bounded Model Checking (BMC) is a formal verification technique used to check whether a system satisfies a given specification by examining its behavior over a limited number of execution steps. This technique works by systematically exploring all possible states of a system up to a predefined bound. If a counterexample is found within this bound, the system is deemed incorrect. If no errors are detected within the specified number of steps, the system is provisionally considered correct—though this conclusion is limited by the bound.

The concept of a completeness threshold (CT) addresses this limitation. A completeness threshold  k  is the number of steps after which, if no errors are found, the system can be considered fully verified with respect to the checked property. Beyond this threshold, the system is guaranteed to be correct for all possible executions, removing the need for further exploration. In the literature, CTs are also referred to as Cut-Offs, Small Worlds, or Small Models.

Goal

This topic offers the opportunity to explore various aspects of completeness thresholds in BMC, with potential research questions including:

• Comparison with Other Termination Guarantees: How do completeness thresholds compare to other formal verification termination guarantees, e.g., widening in abstract interpretation?

• Resource Trade-offs: What are the trade-offs between increasing the bound in BMC and the computational resources required (e.g., time, memory)? At what point does increasing the bound become inefficient? We recommend to experiment with a software model checker like CBMC.

• Practicality of CTs: What is the practical size of completeness thresholds in typical BMC applications? How does this size impact the feasibility of using BMC for larger or more complex systems?

• Domain-Specific Challenges: How do the challenges of applying completeness thresholds in software model checking differ from those in other domains, such as model checking linear temporal logic (LTL) properties in finite-state transition systems?

• Related Concepts in Testing: Are there concepts in the domain of testing (e.g., coverage criteria) that provide similar formal guarantees to completeness thresholds?

Starting Points

• Symbolic Model Checking without BDDs SAT-based bounded model checking
• CBMC bounded model checker for C
• EBMC bounded model checker for Verilog, can compute CTs
• Completeness and Complexity of Bounded Model Checking Introduction of Completeness Thresholds for Finite Transition Systems
• Linear Completeness Thresholds for Bounded Model Checking
• Completeness Thresholds for Memory Safety of Array Traversing Programs
• Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
  • Sec 2.2: State of the art of CTs, contains pointers about CT approximation
  • Sec 4: CTs for software verification
  • Sec C: CT formalization
  • Sec D: Generalized CTs