PDR (Property-Directed Reachability)

aria.efmc.engines.pdr provides a Property-Directed Reachability (IC3) verification engine for transition systems.

Current engine surface

The package exposes:

  • PDRProver

It operates over aria.efmc.sts.TransitionSystem and returns results through VerificationResult.

Idea

PDR (also known as IC3) proves safety by searching for an inductive invariant that is reachable from the initial states, preserved by transitions, and disjoint from unsafe states. Rather than implementing IC3 from scratch, the current engine encodes the verification problem as Constrained Horn Clauses (CHC) and delegates the PDR search to Z3’s HORN solver.

The encoding constructs three Horn clauses over an uninterpreted predicate inv:

  • Init: ∀ vars. init(vars) ⟹ inv(vars)

  • Inductive: ∀ vars, vars'. inv(vars) ∧ trans(vars, vars') ⟹ inv(vars')

  • Post: ∀ vars. inv(vars) ⟹ post(vars)

When Z3 finds a satisfying model, inv is extracted as the inductive invariant. Supported variable sorts include Int, Real, BitVec, and Bool.

Programmatic usage

from aria.efmc.engines.pdr import PDRProver
from aria.efmc.sts import TransitionSystem

sts = TransitionSystem(...)
prover = PDRProver(sts)
prover.set_verbose(True)
result = prover.solve(timeout=60)

if result.is_safe:
    print("Invariant:", result.invariant)
elif result.is_unknown:
    print("Unknown (may have timed out)")

CLI usage

Use the EFMC frontend:

aria-efmc --lang chc --engine pdr --file program.smt2

For exact flags see aria.cli.efmc_cli.