Playing wiht Program Verification with EFMC

This tutorial provides a step-by-step guide to program verification using EFMC.

1. Setup and Installation

First, ensure you have EFMC installed:

# Create and activate a virtual environment (recommended)
python -m venv venv
source venv/bin/activate  # On Unix/macOS
# or
.\venv\Scripts\activate  # On Windows

# Install EFMC
pip install -e .

2. Understanding Input Formats

EFMC supports two main input formats:

  1. CHC (Constrained Horn Clauses)

  2. SyGuS (Syntax-Guided Synthesis)

Example CHC File

Here’s a simple example (fib04_32u.smt2):

(set-logic HORN)
(declare-fun inv ((_ BitVec 32) (_ BitVec 32) ) Bool)
(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
       (=> ( = x ( bvadd (_ bv1 32) ( bvnot (_ bv50 32) ) ) ) (inv x y))))
(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32)) (x! (_ BitVec 32)) (y! (_ BitVec 32)))
       (=> (and (inv x y) ( or ( and ( bvult x (_ bv0 32) ) ( = x! ( bvadd x y ) ) ( = y! ( bvadd y (_ bv1 32) ) ) ) ( and ( bvuge x (_ bv0 32) ) ( = x! x ) ( = y! y ) ) )) (inv x! y!))))
(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32)))
       (=> (inv x y) ( => ( not ( bvult x (_ bv0 32) ) ) ( bvuge y (_ bv0 32) ) ))))
(check-sat)

This example represents:

  • Program with two variables: x and y

  • Initial condition: x = -50

  • Property to verify: When x ≥ 0, then y ≥ 0

3. Basic Verification

Running Verification

You can verify programs using different engines:

  1. Template-based Verification:

    efmc --engine ef --template bv_interval --lang chc --file your_file.smt2

  2. PDR (Property-Directed Reachability):

    efmc --engine pdr --lang chc --file your_file.smt2

  3. K-Induction:

    efmc --engine kind --lang chc --file your_file.smt2

  4. LLM4Inv (LLM-guided Invariant Synthesis):

    efmc --engine llm4inv --lang chc --file your_file.smt2

Understanding Results

The verifier outputs one of these results:

  • safe: Property is verified (program is safe)

  • unsafe: A bug is found

  • unknown: Verifier cannot determine the result

4. Advanced Verification Techniques

K-Induction

K-induction extends basic inductive verification by considering k consecutive states:

efmc --engine kind --k 3 --lang chc --file your_file.smt2

Template-Based Verification

Supports different templates:

Integer/Real Templates: - interval, power_interval: Interval constraints - zone, power_zone: Zone constraints - octagon, power_octagon: Octagonal constraints - affine, power_affine: Affine constraints - poly, power_poly: Polyhedral constraints

Bitvector Templates: - bv_interval, power_bv_interval: Bit-vector intervals - bv_zone, power_bv_zone: Bit-vector zones - bv_octagon, power_bv_octagon: Bit-vector octagons - bv_poly, power_bv_poly: Bit-vector polyhedra - knownbits: Known bits analysis - bitpredabs: Bit-level predicate abstraction - bv_pattern, power_bv_pattern: Pattern-based templates - bv_xor_parity, power_bv_xor_parity: XOR parity templates - bv_rotation, power_bv_rotation: Rotation templates

Floating-Point Templates: - fp_interval: Floating-point intervals - fp_poly: Floating-point polyhedra

Example:

efmc --engine ef --template bv_poly --lang chc --file your_file.smt2

Property-Directed Reachability (PDR)

Uses Z3’s Spacer engine for incremental invariant building:

efmc --engine pdr --lang chc --file your_file.smt2

5. Best Practices

Input Format Guidelines

  1. Use clear variable naming

  2. Specify precise pre and post-conditions

6. Example Workflow

Try different engines:

# Try PDR efmc –engine pdr –lang chc –file your_file.smt2

# Try k-induction efmc –engine kind –kind-k 30 –lang chc –file your_file.smt2

# Try template-based approach efmc –engine ef –template bv_interval –lang chc –file your_file.smt2

# Try LLM4Inv with remote model efmc –engine llm4inv –llm4inv-provider remote –llm4inv-remote-model deepseek-v3 –lang chc –file your_file.smt2

# Try LLM4Inv with local model efmc –engine llm4inv –llm4inv-provider local –llm4inv-local-model qwen/qwen3-coder-30b –lang chc –file your_file.smt2

7. References

  1. Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model checking. MIT press.

  2. Bradley, A. R., & Manna, Z. (2007). The Calculus of Computation: Decision Procedures with Applications to Verification.

  3. Sheeran, M., Singh, S., & Stålmarck, G. (2000). Checking safety properties using induction and a SAT-solver.