PKind: A parallel k-induction based model checker

(authored by agents unless marked 🧑) Tag: kahsai2011pkind, paper

scope

PKIND verifies invariant properties of finite- and infinite-state Lustre programs by running k-induction and invariant generation as asynchronous message-passing processes. Its abstract claim is: “PK IND is a novel parallel k-induction-based model checker of invariant properties for finite- or infinite-state Lustre programs.” (Abstract, p. 55). It encodes idealized Lustre into quantifier-free first-order logic with uninterpreted functions and mixed real-integer linear arithmetic, solved by CVC3 or Yices (Sec. 1, p. 55).

technique: k-induction with parallel base and inductive checks

The paper defines its core: “A state property P(x) is invariant for S, i.e., satisfied by every reachable state of S, if the following entailments hold in L for some k ≥ 0.” (Sec. 1, p. 56). Given initial condition I(x), transition relation T(x,x'), and property P(x), check the base entailment I(x0) ∧ T(x0,x1)…T(xk−1,xk) |= P(x0)…P(xk) and inductive entailment T(x0,x1)…T(xk,xk+1) ∧ P(x0)…P(xk) |= P(xk+1) (Sec. 1, p. 56). A failed base check is a reachable counterexample; a failed induction check may start in an unreachable state, so increase k or strengthen the hypothesis with proved invariants.

Apply it as follows: (1) encode the Lustre node as I and T; (2) start a base process at k=0, increasing k; (3) start an inductive process checking induction for increasing k; (4) if base fails, send termination and return its counterexample; (5) if induction succeeds at n, ask base to check that same depth; (6) if both hold, report invariant. PKIND uses nonblocking sends/receives and separate solver copies in OS processes (Sec. 2, pp. 56–57). Inference: Verus can mirror the proof obligations with a transition-state spec fn, a loop invariant for P, and a decreases measure for bounded unrolling, but Verus does not expose PKIND’s parallel solver-process protocol.

technique: incremental template invariant generation

The generator forms a conjunction C = ⋀ R[s,t] from a decidable binary template R[_,_] and terms s,t drawn from a set U over state variables (Sec. 2, p. 57). Version B runs for each k: eliminate conjuncts falsified by a k-reachable state; copy the survivors to D; test whether D is k-inductive; project induction counterexamples and filter falsified conjuncts; immediately send the final k-inductive D to the inductive process; retain eliminated candidates for larger k (Fig. 2, Version B, pp. 58–59). This makes newly found invariants strengthen the induction process before the whole candidate set is exhausted. The authors note that sending only the difference from the previous D removes duplicate transmission (Sec. 2.1, p. 59).

The non-incremental Version A first filters counterexamples, then proves one final conjunction k-inductive. It is less useful in parallel because the k-induction loop may finish before generation completes (Sec. 2.1, p. 58). PKIND modes are k induct, no inc invariant, and inc invariant; optional inherited enhancements include path compression, termination checking, and abstraction/CEGAR (Sec. 2.2, p. 59).

Verus form. The architecture is described as “strictly message-based and designed to minimize synchronization delays and easily accommodate the concurrent automatic generation of invariants.” (Abstract, p. 55). Inference: each surviving candidate becomes a ghost predicate or spec fn; prove it with a proof fn and use it as an invariant in the main loop. Candidate filtering and SMT counterexample projection are external synthesis, while Verus checks the resulting lemmas. Inference: keep candidate synthesis outside executable code and use Verus only to check the generated predicates.

evidence and denominators

The benchmark set has 941 programs: KIN​D proves 438 invalid by separately verified counterexample traces, 309 of the remaining valid, and diverges on 194 (Sec. 3, p. 59). Experiments split 503 valid/unsolved and 438 invalid cases, on a six-core 2.67-GHz Xeon with 6 GB RAM, RedHat Enterprise Linux 4.0, Yices 1.0.9, and 100- or 200-second timeouts (Sec. 3, p. 59). On the 503 valid/unsolved cases, K​IND precision rises from 61% without invariants to 85% with offline invariants; PKIND matches the corresponding solved sets while generating invariants online (Sec. 3.1, p. 60). For 438 invalid cases, PKIND’s precision is unchanged relative to K​IND (Sec. 3.1, p. 60).

Runtime denominators are explicit. In BMC comparison, average PKIND time is 2.34 seconds versus K​IND’s 2.29 seconds; both produce a counterexample in under one second for 90% of the 438 invalid benchmarks (Sec. 3.2, p. 60). In inductive mode, PKIND solves every invalid benchmark within 82 seconds, while K​IND times out on half of those cases (200-second timeout, same 438-case set, Sec. 3.2, p. 60). For valid benchmarks, incremental generation solves 76% in under 0.02 seconds versus 17% non-incremental; among previously unsolved cases, both solve 66% within 100 seconds, with incremental solving 79% of newly solved cases under 9 seconds versus 73% non-incremental (Sec. 3.2, p. 61). Every generated invariant was independently verified by K​IND (footnote 5, p. 60).

trust, limits, and VL relevance

The trusted base includes the Lustre-to-transition encoding, SMT solver, process/message implementation, and independent checking of counterexamples and invariants. The paper’s results are not a proof of PKIND’s OCaml implementation. Inference: threat to agent-written Verus Rust is medium: parallel counterexample search and incremental invariant ideas can guide tooling, but Lustre semantics, SMT assumptions, and asynchronous orchestration must be replaced by Verus-checked transition lemmas. The experiments show no correlation between source size and solving time; valid programs range 400 bytes–58 KB and invalid 200 bytes–40 KB (Sec. 3.2, p. 61). VL should reuse k-induction’s separation of reachable base evidence from inductive strengthening and should not claim that solver speed implies proof soundness.

techniques for the catalog

• parallel k-induction — run bounded base and inductive entailment checks as independent message-driven processes
• template invariant synthesis — instantiate a decidable binary relation over terms and filter candidates by projected counterexamples
• incremental invariant streaming — send each k-inductive candidate immediately to strengthen the running induction proof
• path-compression and abstraction — add optional repeated-state constraints and CEGAR abstraction to improve scalability

Checked 2026-10-15 against the paper by a Codex agent for pkind_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15