View Source Why SMT Solvers? A Deep Dive into Formal Verification

Table of Contents

  1. Introduction
  2. What is an SMT Solver?
  3. Z3: The State-of-the-Art SMT Solver
  4. SMT Solvers and Code Quality
  5. Verification of Data-Aware Processes
  6. FSM Verification in Cure
  7. Practical Examples
  8. Integration Strategy
  9. Further Reading

Introduction

Modern software systems are growing increasingly complex, with state machines, concurrent processes, and intricate data dependencies. Traditional testing approaches—while valuable—cannot exhaustively verify all possible execution paths and states. This is where Satisfiability Modulo Theories (SMT) solvers become indispensable tools for formal verification.

The Cure language, with its built-in support for finite state machines (FSMs), dependent types, and refinement types, is uniquely positioned to benefit from SMT-based verification. This document explores how SMT solvers, particularly Z3, can dramatically improve code quality and provide mathematical guarantees about program correctness.

Understanding SMT-Solvers: A Simple Introduction

Imagine a puzzle where certain rules must always be obeyed, and the goal is to find out if there’s any way to make all the pieces fit without breaking any rules. SMT-solvers, short for Satisfiability Modulo Theories solvers, are special computer programs designed to solve these rule-based puzzles automatically[^1][^2].

In practical terms, SMT-solvers answer questions like: "Given all the rules (mathematical, logical, or data-related), is there any combination of values that keeps everything true and consistent?" For example, they can check if a set of formulas describing a piece of software will ever run into errors, if a digital circuit will always work correctly, or even if a robot can safely move given complicated obstacles and instructions[^1].

What makes SMT-solvers powerful is that rather than just working with basic true/false logic, they also understand deeper mathematical topics—like arithmetic, relationships between data, and more. They look at every part of the puzzle, combining logic and math, to figure out whether a solution exists or not. If the puzzle can’t be solved, they can even help you pinpoint exactly why it fails[^1][^2].

Satisfiability Modulo Theories (SMT) Solvers in Critical Development

SMT-solvers are computational systems that determine whether statements involving variables and constraints are satisfiable under a range of mathematical theories (such as arithmetic, arrays, bit-vectors, and more)[^3][^4].

What Are SMT-Solvers?

SMT-solvers generalize SAT-solvers (Boolean satisfiability) to additional, expressive theories. This enables the automated analysis of formulas that capture constraints and properties found in realistic software, hardware, and business systems.[^3][^4]

  • Defining Role: They solve logic formulas containing variables and constraints from chosen mathematical theories, checking if any satisfying assignment exists.[^3]
  • Use Domains: These include data-aware workflows, software correctness, circuit design, security analysis, and AI planning.[^3][^4]

See below for more detailed description.

Why SMT-Solvers Matter in Critical Development

SMT-solvers are fundamental in modern software and systems engineering, particularly for safety-critical and high-assurance domains:

  • Rigorous Verification: They automate model checking and formal verification, proving that systems behave correctly in all cases—essential in aviation, medicine, and finance.[^3][^4]
  • Bug & Vulnerability Discovery: Developers encode requirements and invariants as logical formulas; SMT-solvers uncover bugs, unreachable states or vulnerabilities automatically.[^3][^4]
  • Design Optimization & Synthesis: They search huge design spaces for feasible solutions under constraints.
  • Productivity & Reliability: Engineers delegate difficult formal reasoning, focusing on design and innovation.[^3][^4]

Key Educational Source: Alessandro Gianola’s Research

A foundational resource for using SMT-solvers in system verification is Alessandro Gianola’s work, especially his dissertation “SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications.”[^3]

  • Summary: Gianola’s research bridges the gap between model checking for infinite-state systems and verification of data-aware business processes. It shows how SMT-solvers (and their underlying logic frameworks) enable verification of workflows and processes that depend on both control flow and rich data.[^3][^4]
  • Practical Impact: Gianola’s methods use SMT to encode and verify properties (like safety) for processes with both data and state logic, allowing exhaustive and scalable analysis even when manual checking is impossible.[^3][^4]
  • Additional Reading: See Gianola’s thesis and related publications for algorithms, theoretical models, and benchmarking of SMT-verification tools.

Z3: Leading SMT-Solver

Currently, Z3 from Microsoft Research is seen as the most advanced and robust SMT-solver:

  • Theory Coverage: Supports integers, reals, arrays, bit-vectors, and uninterpreted functions.
  • Performance & Integration: Fast solving engines, modern APIs for Python, C++, Java, and more.
  • Community Usage: Z3 is open-source and prominent in both academic research and industrial applications.[^4]

What is an SMT Solver (Part II)?

The Foundation: SAT Solvers

A SAT (Boolean Satisfiability) solver determines whether a Boolean formula can be satisfied—that is, whether there exists an assignment of variables that makes the formula true. For example:

(A ∨ B) ∧ (¬A ∨ C) ∧ (¬B ∨ ¬C)

A SAT solver would find that A = true, B = false, C = true satisfies this formula.

Beyond Boolean: SMT Solvers

SMT (Satisfiability Modulo Theories) solvers extend SAT solvers to handle richer logical theories beyond pure Boolean logic. These theories include:

  • Linear Arithmetic: x + 2y ≤ 5, 3a - b = 7
  • Arrays: select(store(a, i, v), i) = v
  • Bit-vectors: Operations on fixed-width integers
  • Uninterpreted Functions: Abstract function symbols
  • Algebraic Datatypes: Recursive structures like lists and trees
  • Strings: String operations and constraints
  • Quantifiers: ∀x, ∃y predicates

How SMT Solvers Work

SMT solvers typically employ a lazy SMT approach:

  1. Abstract the problem into a Boolean SAT formula
  2. Solve the Boolean formula using an efficient SAT solver
  3. Check if the solution is consistent with the background theories
  4. If inconsistent, add theory lemmas and repeat

This architecture combines the efficiency of modern SAT solvers with the expressiveness of domain-specific theories.

Z3: The State-of-the-Art SMT Solver

Overview

Z3 is a high-performance SMT solver developed by Microsoft Research. It has become the de facto standard for program verification, symbolic execution, and formal methods research.

Key Features

  1. Multiple Theories: Supports arithmetic, arrays, bit-vectors, algebraic datatypes, and more
  2. Quantifier Support: Sophisticated instantiation heuristics for universal/existential quantifiers
  3. Optimization: Can find optimal solutions (maximize/minimize objectives)
  4. Proof Generation: Produces proofs that solutions are correct
  5. Multiple Interfaces: APIs for C, C++, Python, OCaml, Java, .NET, and more
  6. Active Development: Continuously improved with cutting-edge research

Z3 Architecture 

┌─────────────────────────────────────────────┐
│           User Interface (APIs)             │
├─────────────────────────────────────────────┤
│         SMT-LIB 2.0 Parser                  │
├─────────────────────────────────────────────┤
│     Preprocessing & Simplification          │
├─────────────────────────────────────────────┤
│         Core SAT Solver (DPLL)              │
├───────────┬─────────────┬───────────────────┤
│ Arithmetic│   Arrays    │   Datatypes       │
│  Theory   │   Theory    │   Theory          │
│  Solver   │   Solver    │   Solver          │
└───────────┴─────────────┴───────────────────┘

Why Z3?

  • Proven Track Record: Used in Windows driver verification, .NET static analysis, and numerous academic projects
  • Performance: Consistently wins SMT-COMP competitions
  • Extensibility: Easy to integrate into custom verification tools
  • Documentation: Comprehensive guides and active community

SMT Solvers and Code Quality

The Testing vs. Verification Spectrum 

Testing                                    Formal Verification
  │                                              │
  ├─── Unit Tests                                │
  ├─── Integration Tests                         │
  ├─── Property-Based Tests                      │
  ├─── Symbolic Execution ────────────────────┐  │
  │                                           │  │
  │                                           ▼  ▼
  │                                         SMT Solver
  │                                               │
  └───────────────────────────────────────────────┘
         Partial Coverage              Complete Guarantees

How SMT Improves Code Quality

1. Exhaustive Path Coverage

Traditional testing explores a finite set of execution paths. SMT-based verification considers all possible paths symbolically.

Example: Verifying array bounds (below is pseudocode)

# Without SMT: Hope you tested enough edge cases
def access_array(arr: Vector(Int, n), idx: Int): Int =
  arr[idx]  # Runtime check: idx < n ?

# With SMT: Compile-time guarantee
def access_array(arr: Array(Int, n), idx: {i: Int | 0 <= i < n}): Int =
  arr[idx]  # Provably safe - no runtime check needed!

2. Finding Subtle Bugs

SMT solvers excel at finding corner cases that humans miss.

[TODO] Fins an example for that

3. Proving Absence of Errors

Instead of finding bugs, SMT can prove no bugs exist under specified conditions.

Example: Division by zero

# Without SMT: Runtime check required
def divide(x: Int, y: Int): Int =
  match y == 0 do
    true -> error("Division by zero")
    false -> ok(x / y)
  end

# With SMT: Compile-time guarantee via guard
def safe_divide(x: Int, y: Int): Int when y != 0 = x / y
# SMT solver verifies y != 0 before allowing division

4. Guard Completeness Verification ✅

Cure uses SMT solvers to verify that function guards cover all possible input values:

Example: Complete guard coverage

# Guards for sign function
def sign(x: Int): Int when x > 0 = 1
def sign(x: Int): Int when x == 0 = 0
def sign(x: Int): Int when x < 0 = -1

# SMT verification: (x > 0) ∨ (x == 0) ∨ (x < 0) ≡ true ✓
# Compiler proves all Int values are covered

Example: Detecting unreachable clauses

# Redundant guard warning
def classify(x: Int): String when x >= 0 = "non-negative"
def classify(x: Int): String when x > 10 = "large"  # Unreachable!
def classify(x: Int): String = "negative"

# SMT detection: (x >= 0) subsumes (x > 10)
# Compiler warning: Second clause will never execute

Implementation: See cure_guard_smt.erl for:

  • Guard completeness checking
  • Subsumption detection
  • Counterexample generation
  • Inconsistent guard detection
type NonZero = x: Int when x != 0

def safe_divide(a: Int, b: NonZero): Int =
  a / b  # Provably safe - Z3 verifies b /= 0 always holds

4. Validating Optimizations

Compilers can use SMT to verify that optimizations preserve semantics.

# Original
def compute_original(x: Int): Int =
  (x + 1) * (x + 1) - x * x - 2 * x

# Optimized
def compute_optimized(x: Int): Int =
  1

# SMT verification: ∀x. compute_original(x) = compute_optimized(x) ✓

5. Specification Compliance

SMT verifies implementations match formal specifications.

# Specification: sorting produces ordered array with same elements
spec def is_sorted(v: Vector(Int, n)): Bool =
  ∀i j. 0 <= i < j < n → v[i] <= v[j]

spec def same_multiset(v1: Vector(Int, n), v2: Vector(Int, n)): Bool =
  ∀x. count(v1, x) = count(v2, x)

# Implementation must satisfy both properties
def sort(arr: Vector(Int, n)): Vector(Int, n)
  ensures is_sorted(result) ∧ same_multiset(arr, result)
  = ...

Verification of Data-Aware Processes

Background: The Gianola Framework

"Verification of Data-Aware Processes via Satisfiability Modulo Theories" by Alessandro Gianola presents a comprehensive framework for verifying systems that combine:

  • Control flow: State machines, workflows, business processes
  • Data manipulation: Variables, databases, external state
  • Infinite state spaces: Unbounded integers, arrays, data structures

This is precisely the problem domain that Cure FSMs inhabit.

Key Insights from Gianola's Work

1. Data-Aware Processes

A data-aware process consists of:

  • A finite set of control states (FSM states)
  • A data schema (variables, types, constraints)
  • Transition guards (conditions on data)
  • Actions (data transformations)

This maps directly to Cure's FSM model:

record TrafficPayload do
  cycles_completed: Int        # Data schema
  timer_events: Int
  emergency_stops: Int
end

fsm TrafficPayload{...} do
  Red --> |timer| Green        # Control states and transitions
  Green --> |timer| Yellow
  Yellow --> |timer| Red
end

2. Verification Problems

Gianola identifies critical verification problems:

  • Reachability: Can we reach a specific state?
  • Safety: Do we always avoid bad states?
  • Liveness: Do we eventually reach good states?
  • Deadlock Freedom: Can the system always make progress?

3. SMT-Based Decision Procedures

The book presents algorithms that reduce these problems to SMT queries:

Reachability(s0, sf):
  ∃ path. path[0] = s0 ∧ path[n] = sf ∧
          ∀i. valid_transition(path[i], path[i+1])

Safety(s0, bad):
  ¬∃ path. path[0] = s0 ∧ ∃i. path[i] ∈ bad

Liveness(s0, good):
  ∀ path from s0. ∃i. path[i] ∈ good

Z3 can solve these queries even with complex data constraints.

4. Bounded Model Checking

For infinite-state systems, bounded model checking explores up to depth k:

Reachable_k(s0, sf):
  Check all paths of length ≤ k from s0 to sf

If no bug found up to depth k, increase k. SMT solvers efficiently handle increasing bounds.

5. Invariant Synthesis

Gianola describes techniques to automatically discover invariants—properties that hold in all reachable states:

# Synthesized invariant for traffic light
invariant TrafficLight:
  ∀ state. cycles_completed >= 0 ∧
           timer_events >= cycles_completed * 3 ∧
           emergency_stops >= 0

Z3's quantifier reasoning helps discover such invariants automatically.

FSM Verification in Cure

Cure's Verification Opportunities

Cure's design makes it ideal for SMT-based verification:

  1. Explicit FSM Definitions: Clear state space and transitions
  2. Dependent Types: Rich type system with refinements
  3. Guards and Actions: Explicitly stated data constraints
  4. Immutability: Functional core simplifies reasoning

Verification Properties for Cure FSMs

Property 1: State Reachability

Problem: Can state S be reached from the initial state?

Cure Example (from 07_fsm_verification.cure):

fsm LightState{cycle_count: 0} do
  Red --> |timer| Green {cycle_count = cycle_count + 1}
  Green --> |timer| Yellow
  Yellow --> |timer| Red
  Red --> |emergency| Red
  Green --> |emergency| Red
  Yellow --> |emergency| Red
end

# Verification query:
# Is Yellow reachable from Red?
# Answer: Yes, via path Red → Green → Yellow

Z3 Encoding:

(declare-datatypes () ((State Red Green Yellow)))
(declare-fun step (State) State)

(assert (or
  (= (step Red) Green)
  (= (step Red) Red)))
(assert (or
  (= (step Green) Yellow)
  (= (step Green) Red)))
(assert (= (step Yellow) Red))

(assert (= Yellow (step (step Red))))  ; Can reach Yellow in 2 steps?
(check-sat)  ; sat → yes, reachable

Property 2: Deadlock Detection

Problem: Is there a state with no outgoing transitions?

Cure Example:

fsm CounterState{count: 0, max_count: 5} do
  Counting --> |increment| Counting {count = count + 1}
  Counting --> |check| Done {when count >= max_count}
  # Done state has no outgoing transitions → DEADLOCK
end

Z3 Encoding:

(declare-datatypes () ((State Counting Done)))
(declare-fun next (State) State)

; Define transitions
(assert (or
  (= (next Counting) Counting)
  (= (next Counting) Done)))

; Check if Done is a deadlock
(assert (= (next Done) Done))  ; No real transition, self-loop
(assert (distinct Done (next Done)))  ; Try to find different next state
(check-sat)  ; unsat → deadlock confirmed

Property 3: Safety Properties

Problem: Can we reach a "bad" state?

Cure Example (from 07_fsm_verification.cure):

record DoorState do
  is_locked: Int      # 1 = locked, 0 = unlocked
  alarm_active: Int   # 1 = active, 0 = inactive
end

fsm DoorState{is_locked: 1, alarm_active: 0} do
  Locked --> |unlock| Unlocked {is_locked = 0, when alarm_active = 0}
  Unlocked --> |lock| Locked {is_locked = 1}
  Locked --> |activate_alarm| LockedWithAlarm {alarm_active = 1}
  LockedWithAlarm --> |deactivate_alarm| Locked {alarm_active = 0}
  # NO transition from LockedWithAlarm to Unlocked
end

# Safety property: ¬(is_locked = 0 ∧ alarm_active = 1)
# "Never unlocked while alarm is active"

Z3 Verification:

(declare-datatypes () ((State Locked Unlocked LockedWithAlarm)))
(declare-fun is_locked (State) Int)
(declare-fun alarm_active (State) Int)

; Define state invariants
(assert (= (is_locked Locked) 1))
(assert (= (alarm_active Locked) 0))
(assert (= (is_locked Unlocked) 0))
(assert (= (alarm_active Unlocked) 0))
(assert (= (is_locked LockedWithAlarm) 1))
(assert (= (alarm_active LockedWithAlarm) 1))

; Check safety property violation
(declare-const s State)
(assert (and (= (is_locked s) 0) (= (alarm_active s) 1)))
(check-sat)  ; unsat → safety property holds!

Property 4: Liveness Properties

Problem: Do we eventually reach a desired state?

Cure Example:

fsm WorkflowState{tasks_completed: 0, total_tasks: 3} do
  Pending --> |start| InProgress {tasks_completed = 0}
  InProgress --> |complete_task| InProgress {
    tasks_completed = tasks_completed + 1
  }
  InProgress --> |finish| Completed {
    when tasks_completed >= total_tasks
  }
end

# Liveness property: ◇Completed
# "Eventually reach Completed state"

Z3 Encoding (using bounded model checking):

; Check if Completed is reachable within k steps
(declare-datatypes () ((State Pending InProgress Completed)))
(declare-fun state (Int) State)
(declare-fun tasks (Int) Int)

; Initial state
(assert (= (state 0) Pending))
(assert (= (tasks 0) 0))

; Transition constraints for k=10 steps
(define-fun transition ((i Int)) Bool
  (or
    (and (= (state i) Pending)
         (= (state (+ i 1)) InProgress)
         (= (tasks (+ i 1)) 0))
    (and (= (state i) InProgress)
         (= (state (+ i 1)) InProgress)
         (= (tasks (+ i 1)) (+ (tasks i) 1)))
    (and (= (state i) InProgress)
         (>= (tasks i) 3)
         (= (state (+ i 1)) Completed))))

; Check if Completed is reachable
(assert (exists ((i Int)) (and (<= 0 i) (<= i 10) (= (state i) Completed))))
(check-sat)  ; sat → liveness holds

Property 5: Data Invariants

Problem: Do data constraints always hold?

Cure Example:

record CounterData do
  count: Int
  max_count: Int
end

fsm CounterData{count: 0, max_count: 10} do
  Active --> |increment| Active {
    count = count + 1,
    when count < max_count  # Guard prevents overflow
  }
end

# Invariant: ∀ state. 0 <= count <= max_count

Z3 Verification:

(declare-const count_before Int)
(declare-const max_count Int)
(declare-const count_after Int)

; Initial invariant
(assert (= count_before 0))
(assert (= max_count 10))
(assert (<= 0 count_before))
(assert (<= count_before max_count))

; Transition preserves invariant
(assert (< count_before max_count))  ; Guard
(assert (= count_after (+ count_before 1)))  ; Action

; Check invariant after transition
(assert (or (< count_after 0) (> count_after max_count)))
(check-sat)  ; unsat → invariant preserved!

Practical Examples

Example 1: Verifying Refinement Types

Cure supports refinement types (from refinement_types.cure):

type Positive = Int when x > 0
type NonZero = Int when x /= 0
type Percentage = Int when x >= 0 and x =< 100

def safe_divide(a: Int, b: NonZero): Int =
  a / b

Z3 Verification of Type Safety:

(declare-const a Int)
(declare-const b Int)

; Precondition: b is NonZero
(assert (not (= b 0)))

; Division is safe
(declare-const result Int)
(assert (= result (div a b)))

; Check if division by zero is possible
(assert (= b 0))
(check-sat)  ; unsat → division is safe

Example 2: Verifying FSM Transition Guards 

record BankAccount do
  balance: Int
  overdraft_limit: Int
end

fsm BankAccount{balance: 1000, overdraft_limit: 500} do
  Active --> |withdraw| Active {
    balance = balance - amount,
    when balance - amount >= -overdraft_limit
  }
end

Z3 Verification: Prove balance never exceeds overdraft limit

(declare-const balance_before Int)
(declare-const overdraft_limit Int)
(declare-const amount Int)
(declare-const balance_after Int)

; Initial condition
(assert (= balance_before 1000))
(assert (= overdraft_limit 500))

; Transition guard
(assert (>= (- balance_before amount) (- overdraft_limit)))

; Action
(assert (= balance_after (- balance_before amount)))

; Verify invariant: balance >= -overdraft_limit
(assert (< balance_after (- overdraft_limit)))
(check-sat)  ; unsat → invariant holds

Example 3: Proving Equivalence of FSM Refactorings

Original FSM:

fsm TrafficLight1{...} do
  Red --> |timer| Green
  Green --> |timer| Yellow
  Yellow --> |timer| Red
end

Refactored FSM:

fsm TrafficLight2{...} do
  State0 --> |timer| State1
  State1 --> |timer| State2
  State2 --> |timer| State0
end

Z3 Verification: Prove both FSMs are isomorphic

; Define mapping: Red ↔ State0, Green ↔ State1, Yellow ↔ State2
(declare-fun map (State1) State2)

(assert (= (map Red) State0))
(assert (= (map Green) State1))
(assert (= (map Yellow) State2))

; Verify transitions are preserved
(assert (= (map (transition1 Red)) (transition2 (map Red))))
; ... (similar for all transitions)

(check-sat)  ; sat → FSMs are equivalent

Example 4: Detecting Race Conditions in Concurrent FSMs 

record SharedCounter do
  value: Int
end

fsm Counter1{value: 0} do
  Idle --> |increment| Idle {value = value + 1}
end

fsm Counter2{value: 0} do
  Idle --> |increment| Idle {value = value + 1}
end

# Both FSMs share the same `value` variable
# Can concurrent increments lead to lost updates?

Z3 Verification:

(declare-const value_initial Int)
(declare-const value_fsm1 Int)
(declare-const value_fsm2 Int)
(declare-const value_final Int)

(assert (= value_initial 0))

; FSM1 increments
(assert (= value_fsm1 (+ value_initial 1)))

; FSM2 increments (reads initial value due to race)
(assert (= value_fsm2 (+ value_initial 1)))

; Final value (last write wins)
(assert (or (= value_final value_fsm1) (= value_final value_fsm2)))

; Check if final value could be 1 instead of 2
(assert (= value_final 1))
(check-sat)  ; sat → race condition detected!
; Model: both FSMs read value=0, both write value=1, last write wins

Integration Strategy

Compile-Time Verification

Integrate Z3 into the Cure compiler pipeline:

Cure Source Code
      │
      ▼
  Lexer/Parser
      │
      ▼
   Type Checker  ◄───────┐
      │                  │
      ▼                  │
  FSM Analyzer           │
      │                  │
      ▼                  │
 Generate Z3 Queries     │
      │                  │
      ▼                  │
  Z3 Solver              │
      │                  │
      ├──────────────────┘
      │ (unsat → verify next property)
      ▼
 Report Errors/Proofs
      │
      ▼
  Code Generation

Verification Workflow

  1. Extract FSM Structure: Parse FSM definitions, states, transitions, guards
  2. Generate Verification Conditions: Create Z3 queries for each property
  3. Invoke Z3: Check satisfiability of queries
  4. Report Results:
    • unsat → Property holds ✓
    • sat → Counterexample found ✗
    • unknown → Timeout or undecidable

Cure Compiler Integration Points 

%% In cure_fsm_verifier.erl

-export([verify_fsm/1, check_deadlock/1, check_safety/2, check_liveness/2]).

verify_fsm(FSM) ->
    %% Extract FSM structure
    States = extract_states(FSM),
    Transitions = extract_transitions(FSM),
    Guards = extract_guards(FSM),
    
    %% Generate Z3 context
    Z3Context = z3:mk_context([]),
    
    %% Encode FSM in Z3
    StateSort = encode_states(Z3Context, States),
    TransitionAssertions = encode_transitions(Z3Context, StateSort, Transitions),
    
    %% Check properties
    DeadlockResult = check_deadlock(Z3Context, StateSort, Transitions),
    SafetyResult = check_safety_properties(Z3Context, FSM),
    LivenessResult = check_liveness_properties(Z3Context, FSM),
    
    %% Report
    {DeadlockResult, SafetyResult, LivenessResult}.

check_deadlock(Z3Context, StateSort, Transitions) ->
    Solver = z3:mk_solver(Z3Context),
    
    %% For each state, check if it has outgoing transitions
    lists:map(fun(State) ->
        HasTransition = has_outgoing_transition(State, Transitions),
        case HasTransition of
            false -> {deadlock, State};
            true -> ok
        end
    end, get_all_states(StateSort)).

Optimization: Incremental Verification

For large FSMs, use Z3's incremental solving:

verify_incremental(FSM) ->
    Z3Ctx = z3:mk_context([]),
    Solver = z3:mk_solver(Z3Ctx),
    
    %% Add base constraints
    z3:solver_assert(Solver, base_constraints(FSM)),
    
    %% Check properties incrementally
    lists:map(fun(Property) ->
        z3:solver_push(Solver),  % Save state
        z3:solver_assert(Solver, property_constraint(Property)),
        Result = z3:solver_check(Solver),
        z3:solver_pop(Solver),   % Restore state
        {Property, Result}
    end, properties_to_check(FSM)).

IDE Integration

Provide real-time verification feedback in development:

┌─────────────────────────────────────────────┐
│ fsm DoorLock{...} do                        │
│   Locked --> |unlock| Unlocked              │
│   LockedWithAlarm --> |unlock| Unlocked     │ ⚠️ Safety violation
│   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^   │    Can unlock with
│   Warning: Violates safety property         │    alarm active
│ end                                         │
└─────────────────────────────────────────────┘

Testing and Verification Combined

Generate test cases from Z3 counterexamples:

generate_test_from_counterexample(FSM, Property, Counterexample) ->
    %% Z3 provides: [Red, Green, Yellow, Failure]
    TestSteps = lists:map(fun(State) ->
        Event = get_transition_event(State, Counterexample),
        {send_event, Event, expect_state, State}
    end, Counterexample),
    
    %% Generate EUnit test
    generate_eunit_test(FSM, Property, TestSteps).

Further Reading

Books

  1. "Verification of Data-Aware Processes via Satisfiability Modulo Theories" by Alessandro Gianola

    • Comprehensive treatment of SMT-based verification for stateful systems
    • Covers reachability, safety, liveness, and deadlock detection
    • Presents decision procedures and complexity results
    • Essential reading for understanding Cure FSM verification

  2. "The Calculus of Computation" by Aaron R. Bradley and Zohar Manna

    • Foundations of program verification
    • SMT-based verification techniques
    • Temporal logic and model checking

  3. "Decision Procedures" by Daniel Kroening and Ofer Strichman

    • In-depth treatment of SAT and SMT algorithms
    • Theory solvers and their combination
    • Practical implementation details

Papers

  1. "Z3: An Efficient SMT Solver" by Leonardo de Moura and Nikolaj Bjørner

    • Architecture and algorithms of Z3
    • Performance optimizations

  2. "Satisfiability Modulo Theories: Introduction and Applications" by Clark Barrett et al.

    • Overview of SMT landscape
    • Applications in verification

  3. "Temporal Verification of Reactive Systems: Safety" by Zohar Manna and Amir Pnueli

    • Safety properties and their verification
    • Temporal logic foundations

Online Resources

  1. Z3 Tutorial: https://rise4fun.com/z3/tutorial
  2. SMT-LIB Standard: http://smtlib.cs.uiowa.edu/
  3. Z3 API Documentation: https://z3prover.github.io/api/html/
  4. Z3 GitHub Repository: https://github.com/Z3Prover/z3
  1. Dafny: Verification-aware programming language using Z3
  2. CBMC: Bounded model checker for C/C++ using SAT/SMT
  3. Boogie: Intermediate verification language with Z3 backend
  4. Why3: Platform for deductive program verification with SMT support

Conclusion

SMT solvers, particularly Z3, represent a transformative technology for ensuring software correctness. By integrating Z3 into the Cure compiler, we can:

  • Eliminate entire classes of bugs through compile-time verification
  • Provide mathematical guarantees about FSM behavior
  • Catch subtle errors that testing would miss
  • Enable confident refactoring with equivalence proofs
  • Generate high-quality test cases from counterexamples

As Cure evolves, SMT-based verification will become increasingly valuable, especially for mission-critical systems where correctness is paramount. The combination of Cure's expressive type system, built-in FSMs, and Z3's powerful reasoning capabilities creates a uniquely robust platform for building reliable concurrent systems.

The insights from Gianola's "Verification of Data-Aware Processes via Satisfiability Modulo Theories" provide a solid theoretical foundation for implementing these verification techniques in Cure. By following the frameworks and algorithms presented in that work, we can build a world-class verification system that makes Cure a leader in verified systems programming for the BEAM.

References

[^1]: Sudoku and Satisfiability Modulo Theories: Layman’s Example [^2]: Satisfiability Modulo Theories: A Beginner's Tutorial [^3]: Alessandro Gianola, "SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications," PDF. [^4]: Alessandro Gianola et al., “SMT-based Safety Verification of Data-Aware Processes,” CEUR Workshop Proceedings. PDF.

For questions or contributions to Cure's verification infrastructure, please see the project repository and documentation.