Model Checker

Implements bounded model checking using SAT/SMT solvers.

When to Use

• Concurrent program verification
• Protocol verification
• Hardware verification
• Bug detection

What This Skill Does

1. Encodes transitions - To SAT/SMT
2. Unwinds loops - Bounded exploration
3. Checks properties - Safety, liveness
4. Generates counterexamples - For violations

Implementation

from dataclasses import dataclass, field
from typing import Dict, List, Set, Optional
import z3

@dataclass
class State:
    """Program state"""
    pc: int  # Program counter
    vars: Dict[str, int]  # Variables

@dataclass
class Transition:
    """State transition"""
    from_state: State
    to_state: State
    condition: Optional[z3.BoolRef] = None

@dataclass
class Model:
    """Transition system"""
    states: Set[State]
    initial: Set[State]
    transitions: List[Transition]
    variables: List[str]

@dataclass
class Property:
    """Temporal property"""
    pass

@dataclass
class Invariant(Property):
    """Invariant: always P"""
    predicate: z3.BoolRef

@dataclass
class Reachability(Property):
    """Eventually reach: ◇P"""
    predicate: z3.BoolRef

class BoundedModelChecker:
    """Bounded model checker"""
    
    def __init__(self):
        self.solver = z3.Solver()
        self.model: Optional[Model] = None
        self.bound: int = 0
    
    def check(self, model: Model, property: Property, 
              bound: int = 10) -> 'CheckResult':
        """
        Bounded model checking
        
        Returns: (sat/unsat, counterexample if sat)
        """
        
        self.model = model
        self.bound = bound
        
        match property:
            case Invariant(pred):
                return self.check_invariant(pred, bound)
            
            case Reachability(pred):
                return self.check_reachability(pred, bound)
        
        raise ValueError(f"Unknown property: {property}")
    
    def check_invariant(self, invariant: z3.BoolRef, 
                       bound: int) -> 'CheckResult':
        """
        Check invariant: ⊡P (always P)
        
        Encode: ∧_{i=0}^{k} (state_i → P)
        """
        
        self.solver = z3.Solver()
        
        # Create state variables
        state_vars = self.create_state_variables(bound)
        
        # Encode initial state
        self.encode_initial(state_vars[0])
        
        # Encode transitions
        for i in range(bound):
            self.encode_transition(state_vars[i], state_vars[i+1])
        
        # Encode invariant violation
        for i in range(bound + 1):
            violation = z3.Not(self.encode_state_predicate(state_vars[i], invariant))
            self.solver.add(violation)
        
        # Check
        if self.solver.check() == z3.sat:
            model = self.solver.model()
            return CheckResult(
                sat=True,
                counterexample=self.extract_trace(state_vars, model),
                message="Invariant violated"
            )
        
        return CheckResult(
            sat=False,
            counterexample=None,
            message="Invariant holds within bound"
        )
    
    def check_reachability(self, target: z3.BoolRef,
                          bound: int) -> 'CheckResult':
        """
        Check reachability: ◇P
        
        Encode: ∃i. state_i → P
        """
        
        self.solver = z3.Solver()
        
        state_vars = self.create_state_variables(bound)
        self.encode_initial(state_vars[0])
        
        for i in range(bound):
            self.encode_transition(state_vars[i], state_vars[i+1])
        
        # Target reachable
        target_reached = z3.Bool('target_reached')
        for i in range(bound + 1):
            self.solver.add(
                target_reached == self.encode_state_predicate(state_vars[i], target)
            )
        
        self.solver.add(target_reached)
        
        if self.solver.check() == z3.sat:
            model = self.solver.model()
            return CheckResult(
                sat=True,
                counterexample=self.extract_trace(state_vars, model),
                message="Target reachable"
            )
        
        return CheckResult(
            sat=False,
            counterexample=None,
            message="Target not reachable within bound"
        )
    
    def create_state_variables(self, bound: int) -> List[Dict[str, z3.Expr]]:
        """Create symbolic state variables"""
        
        states = []
        
        for i in range(bound + 1):
            state = {}
            for var in self.model.variables:
                state[var] = z3.Int(f"s{i}_{var}")
            states.append(state)
        
        return states
    
    def encode_initial(self, state: Dict[str, z3.Expr]):
        """Encode initial state constraints"""
        
        for init in self.model.initial:
            for var, val in init.vars.items():
                self.solver.add(state[var] == val)
    
    def encode_transition(self, from_state: Dict[str, z3.Expr],
                        to_state: Dict[str, z3.Expr]):
        """Encode transition relation"""
        
        for trans in self.model.transitions:
            # Match: from_state matches trans.from_state
            # Result: to_state matches trans.to_state
            
            conditions = []
            
            for var in self.model.variables:
                # Simple: copy if not changed
                conditions.append(to_state[var] == from_state[var])
            
            # Add transition-specific constraints
            for var, val in trans.to_state.vars.items():
                if var in from_state and from_state[var] != val:
                    conditions.append(to_state[var] == val)
            
            if trans.condition:
                conditions.append(trans.condition)
            
            self.solver.add(z3.Or(conditions))
    
    def encode_state_predicate(self, state: Dict[str, z3.Expr],
                              pred: z3.BoolRef) -> z3.BoolRef:
        """Encode predicate for state"""
        
        # Substitute state variables into predicate
        subst = {z3.Int(var): val for var, val in state.items()}
        
        return z3.substitute(pred, subst)
    
    def extract_trace(self, states: List[Dict[str, z3.Expr]], 
                     model: z3.Model) -> List[Dict[str, int]]:
        """Extract counterexample trace"""
        
        trace = []
        
        for state in states:
            concrete = {}
            for var, expr in state.items():
                val = model.eval(expr)
                concrete[var] = val.as_long()
            trace.append(concrete)
        
        return trace

@dataclass
class CheckResult:
    """Model checking result"""
    sat: bool
    counterexample: Optional[List[Dict[str, int]]]
    message: str

Concurrent Program Verification

class ConcurrentModelChecker:
    """Model checker for concurrent programs"""
    
    def __init__(self):
        self.checker = BoundedModelChecker()
    
    def verify_two_thread(self, program: 'Program', 
                        property: Property) -> CheckResult:
        """
        Verify program with 2 threads
        
        Interleaving semantics:
        - All possible thread schedules
        - Shared memory consistency
        """
        
        # Model as transition system
        model = self.create_model(program)
        
        # Check with increasing bounds
        for bound in range(1, 20):
            result = self.checker.check(model, property, bound)
            
            if result.sat:
                return result
        
        return CheckResult(
            sat=False,
            counterexample=None,
            message="Property holds (or bound too small)"
        )
    
    def create_model(self, program: 'Program') -> Model:
        """Create transition system model"""
        
        # Extract states and transitions
        states = set()
        initial = set()
        transitions = []
        
        # Initial state
        init_state = State(pc=0, vars=program.init_vars)
        initial.add(init_state)
        states.add(init_state)
        
        # Build transitions from CFG
        for stmt in program.statements:
            from_state = State(stmt.from_pc, stmt.from_vars)
            to_state = State(stmt.to_pc, stmt.to_vars)
            
            trans = Transition(from_state, to_state, stmt.condition)
            transitions.append(trans)
            
            states.add(from_state)
            states.add(to_state)
        
        return Model(
            states=states,
            initial=initial,
            transitions=transitions,
            variables=list(program.variables)
        )

Liveness Checking

class LivenessChecker:
    """Check liveness properties"""
    
    def check_liveness(self, model: Model, property: Reachability) -> CheckResult:
        """
        Check: ◇P (eventually P)
        
        Uses fairness constraints
        """
        
        # Check: can we reach P infinitely often?
        # Add fairness: each thread executes infinitely
        
        # For now, simple bounded version
        checker = BoundedModelChecker()
        
        # Try increasingly larger bounds
        for bound in range(1, 50):
            result = checker.check(model, property, bound)
            
            if result.sat:
                return result
        
        return CheckResult(sat=False, message="Property may not hold")

Key Concepts

Properties

Tips

• Start with small bounds
• Use predicate abstraction
• Handle infinite state with care
• Consider fairness

Related Skills

• symbolic-execution-engine - Symbolic execution
• weak-memory-model-verifier - Memory models
• smt-solver-interface - SMT solving

Canonical References

Tradeoffs and Limitations

Model Checking Approach Tradeoffs

When NOT to Use Model Checking

• For large systems: State explosion; use abstraction
• For parameterized systems: Unbounded verification hard
• For probabilistic systems: Use probabilistic model checking
• For real-time: Use timed automata model checking

Complexity Considerations

• Explicit-state: O(n) states, exponential in variables
• Symbolic: Exponential in worst case, often practical
• BMC: Linear in bound × state size
• SMT solving: NP-hard, but Z3 fast in practice

Limitations

• State explosion: Main bottleneck; exponential in components
• Infinite state: Requires abstraction or bounded checking
• Scalability: Can't handle large software systems
• Liveness: Hard to verify; requires fairness assumptions
• Counterexample: May be too long to understand
• Parameterization: N-process systems hard

Research Tools & Artifacts

Model checking tools:

Key Papers

• Clarke et al. - Model checking papers
• Biere et al. - BMC papers

Research Frontiers

1. Software Model Checking

• Goal: Scale to large codebases
• Approach: Predicate abstraction, abstraction refinement
• Tools: CBMC, ESBMC

Implementation Pitfalls