Symbolic Abstraction

Overview

Symbolic Abstraction is a verification technique that computes the strongest consequence of a formula within a given abstract domain. Unlike template-based approaches that search for invariants by solving constraints, symbolic abstraction iteratively refines an invariant by computing the strongest abstract representation of the current invariant conjoined with the transition relation.

The symbolic abstraction prover in EFMC implements a fixpoint computation that: 1. Starts with the initial condition as the current invariant 2. At each iteration, computes the strongest consequence of the current invariant and transition relation in the chosen abstract domain 3. Takes the disjunction with the previous invariant 4. Continues until a fixpoint is reached 5. Verifies that the computed invariant implies the safety property

Supported Abstract Domains

Interval Domain: - Tracks lower and upper bounds for each variable - Suitable for integer and real variables - Also supports bit-vector intervals

Bits Domain: - Tracks known bits for bit-vector variables - For each bit position, tracks if it must be 0, must be 1, or is unknown - Provides fine-grained bit-level information

Known Bits Domain: - Similar to bits domain but focuses on known bit patterns - More efficient than full bits analysis

Algorithm

The symbolic abstraction algorithm computes the least fixpoint:

\[ \begin{align}\begin{aligned}I_0 = \text{init}\\I_{i+1} = I_i \vee \text{strongest\_consequence}(I_i \wedge \text{trans}, \text{domain})\end{aligned}\end{align} \]

where strongest_consequence computes the strongest formula in the abstract domain that is implied by the input formula.

Usage

The symbolic abstraction prover can be used via the command line:

efmc --engine symabs --symabs-domain interval --lang chc --file program.smt2

For bit-vector programs with bit-level analysis:

efmc --engine symabs --symabs-domain known_bits --lang chc --file program.smt2

Command-Line Options

  • --symabs-domain: Abstract domain to use - interval: Interval abstraction (default) - bits: Full bit-level analysis - known_bits: Known bits analysis

Programmatic Usage

from efmc.engines.symabs import SymbolicAbstractionProver
from efmc.sts import TransitionSystem

# Create transition system
sts = TransitionSystem(...)

# Create prover
prover = SymbolicAbstractionProver(sts)
prover.domain = 'interval'  # or 'bits', 'known_bits'

# Solve
result = prover.solve()

if result.is_safe:
    print(f"System is safe")
    print(f"Invariant: {result.invariant}")
else:
    print("System is unsafe or unknown")

Implementation Details

Bit-Vector Symbolic Abstraction: - Uses interval abstraction for bit-vector variables - Supports signed and unsigned interpretations - Can track overflow and underflow conditions

Bit-Level Symbolic Abstraction: - Analyzes individual bits of bit-vector variables - Tracks known bits (must be 0 or 1) vs unknown bits - More precise but computationally more expensive

Fixpoint Detection: - Uses validity checking to detect when the invariant has converged - Stops when the new invariant implies the previous one

Advantages

  • Precision: Can be more precise than template-based approaches for certain domains

  • Automatic Refinement: Iteratively refines the invariant without manual template selection

  • Domain Flexibility: Supports multiple abstract domains

Limitations

  • Computational Cost: Computing strongest consequences can be expensive

  • Domain Dependency: Precision depends heavily on the chosen abstract domain

  • Convergence: May require many iterations to reach fixpoint