Verification of Configurable SRA Systems

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

problem and result

A scheduler-restricted asynchronous (SRA) system is an unbounded family of asynchronous-process systems generated by legal configurations. The paper proves one global safety property for every configuration by composing local method contracts with first-order entailment checks. Its goal is stated precisely: “Our goal is proving at once that for every legal instantiation, at the end of every scheduling cycle, a given global property holds.” (Sec. 4, p. 8)

The global invariant Inv ranges over all instances and scheduler state. A class receives local contracts for initialization, phase-specific execution, and ticking. The main theorem is: “If all local contracts are valid and all global entailment checks succeed for an invariant Inv , then φ holds at the end of every scheduling cycle in every run of S, for all configurations satisfying Γ .” (Theorem 1, Sec. 4.2, p. 10)

technique 1: contract-based compositional verification

What it is. Verify each class method in isolation, then prove that the scheduler’s interleaving preserves a global invariant. A local contract is a Hoare triple {Pre} m {Post}; old(e) refers to the pre-state value. The generated contracts are {true} init() {IC}, {true} exec(p) {TC(p)}, and {true} tick() {KC} (Sec. 4.2, p. 9).

How to do it.

1. Define configuration constraints Γ, classes, scheduler phases, transition guards, and target safety property φ (Secs. 3–4, pp. 5–8)
2. Generate or write each class’s IC, TC(p), and KC contracts; validate them for every legal configuration and instance (Sec. 4.2, p. 9)
3. Choose a global invariant Inv that implies φ at the final scheduler phase (Sec. 4.2, p. 10)
4. For initialization, prove Γ entails that every initialized instance and phase l0 imply Inv (Sec. 4.2, p. 10)
5. For every phase edge, prove a preservation entailment; final edges additionally apply each KC, and reset edges allow only specified input changes (Sec. 4.2, pp. 10–11)
6. For each scheduler self-loop, reduce arbitrary instance interleavings to one-instance preservation plus induction over the number of executed instances (Sec. 4.2, pp. 9–10)
7. Prove Γ |= Inv ∧ phase=lf ⇒ φ (Sec. 4.2, p. 10)

Verus form (Inference: the paper implements Dafny contracts, not Verus). Map class methods to Rust methods with requires and ensures; represent old values using Verus’s pre-state expressions in postconditions or explicit ghost snapshots. Put Inv in loop invariant clauses and prove one-instance preservation in proof functions. The scheduler’s arbitrary interleaving needs a ghost set of executed instances and an induction lemma; ordinary Rust ownership does not itself prove the global invariant.

Evidence. The theorem proof is induction over scheduler transitions, with an inner induction over interleavings (Appendix C, Sec. 4.2). The paper explicitly says local contracts “can be generated automatically from class definitions and verified independently using standard program verification techniques.” (Sec. 4.2, p. 9)

technique 2: stable per-instance guard abstraction

A global scheduler guard may cease to hold after another instance executes. The paper introduces a local predicate g'p for the current instance. It must satisfy establishment, Γ |= Inv ∧ Gp→p ⇒ c.g'p, and stability under every other instance’s execution, Γ |= old(Inv ∧ c.g'p) ∧ d.TD(p) ∧ d.executed ⇒ c.g'p (Sec. 4.2, p. 9).

Steps.

1. Identify the global facts needed by one instance’s method
2. Define g'p over that instance’s fields
3. Prove establishment from Γ, Inv, and the scheduler guard
4. Prove stability for every other class and instance contract
5. Prove the single-instance entailment old(Inv ∧ phase=p ∧ c.g'p ∧ c.TC(p) ∧ c.executed) ⇒ Inv (Sec. 4.2, p. 9)

The paper gives a simple default: “In practice, a common choice for gp′ is ¬c.executed (instance c has not yet executed in phase p).” (Sec. 4.2, p. 9)

Verus form (Inference). Store executed as ghost state and use a loop invariant stating that unexecuted instances satisfy the local approximation. Prove each execution step preserves the approximation for all untouched instances. Quantified collections may require finite ghost sets and trigger-friendly lemmas; the paper does not address Verus solver triggers.

technique 3: automatic contract generation by symbolic effects

The implementation derives an exec contract from transition code. For each effect E, forward symbolic execution computes a map ME from variables to pre-state expressions. Assignments update map entries, conditionals produce conditional expressions, and quantified assignments produce lambda expressions. Individual transition effects are combined as a disjunction, with guards strengthened by priority constraints (Sec. 5.1, p. 11).

How to apply it.

1. Build a symbolic map initialized to pre-state variables
2. Process each assignment by replacing the target’s map entry
3. Translate each conditional into an if expression over symbolic values
4. Translate quantified field updates into lambda expressions
5. Conjoin each transition guard with the priority condition from the paper
6. Disjoin the resulting guarded effects into TC(p) (Sec. 5.1, p. 11)

Verus form (Inference). Generate a Rust specification function for each transition and prove the executable method’s ensures against the disjunction. This is a generator design, not a built-in Verus feature; generated specs must remain aligned with executable code.

technique 4: quantifier grounding

When Γ bounds a set-valued field, replace quantifiers with finite conjunctions/disjunctions. For |s|=k, expand universal and existential quantification over the k elements; for |s|≤k, use a bounded nullable representation. The rewrite applies both to method code and contracts and is proved equivalent under Γ (Sec. 5.2, pp. 11–12).

Steps.

1. Detect a cardinality constraint in Γ
2. Keep the original set in ghost state
3. Generate a grounded object-valued field, possibly nullable
4. Rewrite quantified code and specifications into finite Boolean formulas
5. Generate equivalence lemmas under size and set/object correspondence assumptions
6. Verify the grounded formulas; transfer the result to the original formulas via equivalence (Sec. 5.2, p. 12)

Verus form (Inference). Use finite sequences or sets in ghost state and expose a bounded element representation to the solver. Prove equivalence with ensures lemmas under cardinality assumptions. This optimization is useful only when the bound is explicit and maintained.

evidence, trusted parts, and limits

Experiments use Dafny 4.11.0 on AMD EPYC 7413 nodes, with 8 GB RAM per verification task (Sec. 6, p. 13). The RCS set encoding has 105 assertions and takes 2 seconds; its list encoding has 994 assertions and takes 4233 seconds, while list plus grounding takes 925 seconds (Table 1, p. 13). For RPS, the grounded set encoding reduces total local-contract time from 729 to 620 seconds (963 assertions in both rows). These denominators and settings are per system/version row, not averages.

The RCS safety property is not inductive initially; manually extending it to an invariant takes 18 seconds and 63.26M Dafny resource-count units (Sec. 6, p. 14). RPS verifies 25 safety properties: 21 reproduced from prior work plus four new engineer properties (Sec. 6, p. 14). Proprietary industrial models cannot be publicly shared (footnote, p. 12), limiting independent reproduction.

Trusted components include Dafny/SMT validity, generated-contract correctness, Γ’s configuration assumptions, and the abstraction from scheduler implementation to the SRA semantics. The paper says finding a suitable invariant reduces to an undecidable parameterized-safety problem (Sec. 4.2, p. 10). Quantifier grounding is sound only under its cardinality and correspondence assumptions.

Inference: the product risk from agent-written verified Rust is material but bounded. The strongest transferable design is contract generation plus a global invariant proof over scheduler phases. Verus can express local contracts and inductive invariants, but the paper does not establish that Verus can automatically handle quantified instance sets or generated lambda effects. A VL product should retain configuration bounds, generated-contract provenance, and invariant assumptions as reviewable artifacts.

techniques for the catalog

• compositional SRA contracts: verify init, phase execution, and tick locally, then preserve a global invariant
• stable guard abstraction: replace a changing global guard with an established and stable per-instance predicate
• symbolic contract generation: compute transition effects as pre-state expressions and guarded disjunctions
• quantifier grounding: rewrite bounded set quantifiers into finite formulas and prove specification equivalence
• scheduler-phase induction: prove initialization, self-loop interleavings, phase edges, final property, and reset separately

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15