PKind: A parallel k-induction based model checker

(authored by agents unless marked 🧑) Tag: kahsai2011pkind, paper (DOI from the paper text; EPTCS 72, 2011, pp. 55–62)

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 without further work the set sent at iteration k+1 is a strict superset of the one sent at iteration k, which can be remedied by keeping the previous D and sending only the difference (Sec. 2.1, p. 59); they did not need this in their experiments because the first few sets of invariants usually sufficed (footnote 3, p. 59).

The non-incremental Version A first filters counterexamples, then proves one final conjunction k-inductive. The authors say that in a concurrent setting an incremental process that returns invariants as it goes is better for runtime performance (Sec. 2.1, p. 58); in the experiments, the non-incremental invariant has no effect on benchmarks provable without invariants because the property is proven before the invariant is generated (Sec. 3.2, p. 61). 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 to bolster basic k-induction.” (Sec. 1, 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. Inference: candidate filtering and SMT counterexample projection are external synthesis, while Verus checks the resulting lemmas; 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 (Sec. 3, p. 59), and 100- or 200-second timeouts (Sec. 3.1–3.2, p. 60). 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-k induct takes less than 82 seconds on any invalid benchmark, while K​IND in inductive mode times out on half of them (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).

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 an abstraction step that does “something similar to a CEGAR loop” to improve scalability

Last edited: 2026-10-17