ESBMC Verification Skill

ESBMC (Efficient SMT-based Context-Bounded Model Checker) detects bugs or proves their absence in C, C++, CUDA, CHERI-C, Python, Solidity, Java, and Kotlin programs.

Prerequisites Check

Before running any ESBMC command, verify that ESBMC is installed by running which esbmc or esbmc --version . If ESBMC is not found, inform the user and provide installation instructions:

• Pre-built binaries: Download from ESBMC releases

• Build from source: Clone https://github.com/esbmc/esbmc and follow the build instructions in its README

• After installing, ensure esbmc is in the PATH: export PATH=$PATH:/path/to/esbmc/bin

Do not proceed with verification commands until ESBMC is confirmed available.

Verification Pipeline

Source Code → Frontend Parser → GOTO Program → Symbolic Execution (SSA) → SMT Formula → Solver → Result

Quick Start

C file with default checks

esbmc file.c

C++ file

esbmc file.cpp

Python (requires type annotations)

esbmc file.py

Solidity contract

esbmc --sol contract.sol --contract ContractName

Common safety checks

esbmc file.c --memory-leak-check --overflow-check --unwind 10 --timeout 60s

Concurrency verification

esbmc file.c --deadlock-check --data-races-check --context-bound 2

Supported Languages

Language Command Notes

C esbmc file.c

Default, Clang frontend

C++ esbmc file.cpp

C++11-20 via --std

Python esbmc file.py

Requires type annotations, Python 3.10+

Solidity esbmc --sol file.sol --contract Name

Smart contracts

CUDA esbmc file.cu

GPU kernel verification

Java/Kotlin esbmc file.jimple

Requires Soot conversion from .class

For language-specific options and examples, see references/language-specific.md .

Safety Properties

Default Checks (Always On)

• Array bounds: Out-of-bounds array access

• Division by zero: Integer and floating-point

• Pointer safety: Null dereference, invalid pointer arithmetic

• Assertions: User-defined assert() statements

Optional Checks (Enable Explicitly)

• --overflow-check / --unsigned-overflow-check : Integer overflow

• --memory-leak-check : Memory leaks

• --deadlock-check / --data-races-check : Concurrency safety

• --nan-check : Floating-point NaN

• --ub-shift-check : Undefined shift behavior

• --is-instance-check : Enable runtime isinstance assertions for annotated Python code

Disable Specific Checks

--no-bounds-check , --no-pointer-check , --no-div-by-zero-check , --no-assertions

For the full CLI reference, see references/cli-options.md .

Loop Invariants and Function Contracts

These features extend ESBMC beyond the reach of plain BMC — use them when BMC hits its scaling limits, not as a general replacement. Both are under active development; encourage users to try them.

When to recommend each

Situation Recommend

Loop with small or known bound --unwind N — simpler, counterexamples are confirmed bugs

Loop bound large / unbounded, BMC times out --loop-invariant --ir

Function called once or twice Plain BMC / k-induction

Function called many times, BMC times out --enforce-contract

• --replace-call-with-contract

What to tell the user before they start

• These are over-approximations — a verification failure may mean the abstraction needs refinement, not that the program has a real bug.

• Iteration is expected and normal. Guide the user through the refinement cycle rather than treating the first failure as a dead end.

• VERIFICATION SUCCESSFUL with a correct abstraction is a sound, trustworthy result.

For the refinement workflow, see references/loop-invariants.md and references/function-contracts.md .

Loop Handling

K-induction is an alternative strategy that bypasses loop discovery entirely — see the Strategy Selection section below. If you are using BMC instead, always start by discovering loops before choosing an unwind strategy. Never guess a bound with --unwind N .

Step 1: discover all loops and their IDs

esbmc file.c --show-loops

Decision tree based on the output:

• No loops → no unwind flag needed; run without any unwind option

• Loops with apparent bounds (e.g., for (i = 0; i < N; i++) ) → use per-loop bounds derived from the source: esbmc file.c --unwindset L1:N,L2:M

• Loops with unknown or dynamic bounds → use incremental BMC: esbmc file.c --incremental-bmc

Strategy Selection

Choose a high-level path before running any checks:

Path A — k-Induction (try first for proving correctness)

• No loop discovery needed.

• Detect CPU count: nproc on Linux, sysctl -n hw.ncpu on macOS.

4 CPUs → use --k-induction-parallel

• ≤4 CPUs → use --k-induction

• If k-induction succeeds → property is proved (unbounded result).

• If k-induction times out or returns UNKNOWN → fall back to Path B.

Path B — BMC (bounded, loop-aware)

• Run --show-loops , then choose --unwindset or --incremental-bmc per the Loop Handling decision tree above.

Verification Strategies

Goal Strategy Command

Loops with known bounds BMC with unwindset --unwindset L1:N,...

Unknown loop bounds Incremental BMC --incremental-bmc

Prove correctness (≤4 CPUs) k-Induction --k-induction

Prove correctness (>4 CPUs) k-Induction parallel --k-induction-parallel

All violations Multi-property --multi-property

Large programs Incremental SMT --smt-during-symex

Concurrent code Context-bounded --context-bound 3

For detailed descriptions of the strategies and their configurations, see references/verification-strategies.md .

Solver Selection

Always detect available solvers via --list-solvers rather than assuming one is present. Use the best available solver by priority: Boolector → Bitwuzla → Z3.

esbmc --list-solvers # Detect available solvers esbmc file.c --boolector # Boolector (highest priority) esbmc file.c --bitwuzla # Bitwuzla (second priority) esbmc file.c --z3 # Z3 (fallback)

If none of these solvers are available, ESBMC was built without solver support and verification cannot proceed.

ESBMC Intrinsics

Use these in the source code to guide verification.

Quick Reference

Purpose C/C++ Python

Symbolic int __ESBMC_nondet_int()

nondet_int()

Symbolic uint __ESBMC_nondet_uint()

N/A

Symbolic bool __ESBMC_nondet_bool()

nondet_bool()

Symbolic float __ESBMC_nondet_float()

nondet_float()

Symbolic string N/A nondet_str()

Symbolic list N/A nondet_list()

Symbolic dictionary N/A nondet_dict()

Assumption __ESBMC_assume(cond)

assume(cond)

Assertion __ESBMC_assert(cond, msg)

esbmc_assert(cond, msg)

Atomic section __ESBMC_atomic_begin/end()

N/A

Basic Usage

int x = __ESBMC_nondet_int(); // Symbolic input __ESBMC_assume(x > 0 && x < 100); // Constrain input __ESBMC_assert(result >= 0, "msg"); // Verify property

x: int = nondet_int() __ESBMC_assume(x > 0 and x < 100) assert result >= 0, "msg"

For the step-by-step process of adding intrinsics to code, see references/adding-intrinsics.md . For the full intrinsics API, see references/intrinsics.md .

Output and Debugging

esbmc file.c # Counterexample shown on failure esbmc file.c --witness-output w.graphml # Generate witness file esbmc file.c --show-vcc # Show verification conditions esbmc file.c --generate-testcase # Generate test from counterexample esbmc file.py --generate-pytest-testcase # Generate pytest

Resource Limits

esbmc file.c --timeout 300s # Time limit esbmc file.c --memlimit 4g # Memory limit

Common Workflows

Bug Hunting

Step 1: discover loops

esbmc file.c --show-loops

Step 2a: known bounds

esbmc file.c --boolector --unwindset L1:N --timeout 60s

Step 2b: unknown bounds

esbmc file.c --boolector --incremental-bmc --timeout 120s

Proving Correctness

Step 1: detect CPUs

nproc # Linux; use sysctl -n hw.ncpu on macOS

Step 2a: >4 CPUs

esbmc file.c --boolector --k-induction-parallel --overflow-check

Step 2b: ≤4 CPUs

esbmc file.c --boolector --k-induction --overflow-check

Step 3: if k-induction times out or returns UNKNOWN, fall back to BMC

esbmc file.c --show-loops # then use --unwindset or --incremental-bmc

Memory Safety Audit

esbmc file.c --boolector --unwindset L1:N --memory-leak-check

Concurrency Verification

esbmc threaded.c --boolector --deadlock-check --data-races-check --context-bound 2

For guidance on fixing verification failures, see references/fixing-failures.md .

Additional Resources

Reference Files

• references/cli-options.md — Complete CLI reference

• references/verification-strategies.md — Detailed strategy guide

• references/language-specific.md — Language-specific features and options

• references/intrinsics.md — Full ESBMC intrinsics API

• references/adding-intrinsics.md — Step-by-step guide for annotating code

• references/fixing-failures.md — Diagnosing and fixing verification failures

• references/loop-invariants.md — Loop invariant syntax, CLI flag, design guidelines, and debugging

• references/function-contracts.md — Function contract clauses, enforce/replace modes, when to use each, and examples

Example Files

• examples/memory-check.c — Memory safety verification (C)

• examples/overflow-check.c — Integer overflow detection (C)

• examples/concurrent.c — Concurrency verification (C)

• examples/cpp-verify.cpp — C++ verification (classes, STL, RAII)

• examples/python-verify.py — Python verification

Scripts

• scripts/quick-verify.sh — Quick verification wrapper

• scripts/full-audit.sh — Comprehensive security audit