BDD-based Symbolic Model Checking¶
The BDD (Binary Decision Diagram) module implements symbolic model checking for Boolean programs using Z3’s Boolean reasoning capabilities. This prover performs both forward and backward reachability analysis to verify safety properties.
Overview¶
BDD-based symbolic model checking is a technique that uses Binary Decision Diagrams to represent and manipulate Boolean functions efficiently. In EFMC, this is implemented using Z3’s Boolean reasoning capabilities rather than traditional BDD libraries.
Algorithm¶
The BDD prover implements two main approaches:
Forward Reachability Analysis: 1. Start with the initial states 2. Iteratively compute the image (successor states) using the transition relation 3. Continue until a fixpoint is reached or the maximum number of iterations is exceeded 4. Check if the computed reachable states satisfy the safety property
Backward Reachability Analysis: 1. Start with the negation of the safety property (bad states) 2. Iteratively compute the pre-image (predecessor states) using the transition relation 3. Continue until a fixpoint is reached or the maximum number of iterations is exceeded 4. Check if the initial states are contained in the computed bad states
Usage¶
The BDD prover can be used as follows:
from efmc.engines.bdd import BDDProver
from efmc.sts import TransitionSystem
# Create transition system
sts = TransitionSystem(...)
# Create BDD prover with forward analysis
prover = BDDProver(sts, use_forward=True, max_iterations=1000)
# Solve the verification problem
result = prover.solve()
if result.is_safe:
print("System is safe")
print(f"Invariant: {result.invariant}")
else:
print("System is unsafe or unknown")
Configuration Options¶
use_forward: Boolean flag to choose between forward (True) and backward (False) analysis
max_iterations: Maximum number of iterations for fixpoint computation (default: 1000)
Limitations¶
Currently uses Z3’s Boolean reasoning rather than dedicated BDD libraries
Future Improvements¶
Integration with dedicated BDD libraries (e.g., CUDD) for better performance