Pith Number

pith:PKMAIL2D

pith:2026:PKMAIL2DPJHUEP75XLX5S5Y762

not attested not anchored not stored refs resolved

Complete Local Reasoning About Parameterized Programs Over Topologies

Azadeh Farzan, Ruotong Cheng

Safety verification of parameterized concurrent programs reduces to complete local proofs under suitable topology assumptions.

arxiv:2605.15143 v1 · 2026-05-14 · cs.LO · cs.PL

Open paper page JSON Open Graph Bundle Merged state What is a Pith Number?

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{PKMAIL2DPJHUEP75XLX5S5Y762}

Prints a linked badge after your title and injects PDF metadata. Compiles on arXiv. Learn more

Record completeness

1 Bitcoin timestamp

2 Internet Archive

3 Author claim open · sign in to claim

4 Citations open

5 Replications open

✓ Portable graph bundle live · download bundle · merged state

The bundle contains the canonical record plus signed events. A mirror can host it anywhere and recompute the same current state with the deterministic merge algorithm.

Claims

C1strongest claim

under reasonable assumptions on the underlying topology, the problem can be reduced to and solved as a compositional scheme, that is, the verification of the parameterized family is reduced to a set of local proofs, in a complete manner.

C2weakest assumption

reasonable assumptions on the underlying topology that enable the complete reduction from global parameterized verification to a finite set of local proofs.

C3one line summary

Parameterized concurrent program safety over topologies reduces to complete local compositional proofs via universally quantified inductive invariants.

References

38 extracted · 38 resolved · 0 Pith anchors

[1] International Journal on Software Tools for Technology Transfer18(5), 469–473 (Oct 2016) 2016 · doi:10.1007/s10009-016-0424-3

[2] In: Giacobazzi, R., Berdine, J., Mastroeni, I 2013 · doi:10.1007/978-3-642-35873-9_28

[3] Distributed Computing31(3), 187–222 (Jun 2018) 2018 · doi:10.1007/s00446-017-0302-6

[4] Information Processing Letters22(6), 307–309 (May 1986) 1986 · doi:10.1016/0020-0190(86)90071-2

[5] (eds.) Computer Aided Verification 2001 · doi:10.1007/3-540-44585-4_19

Formal links

2 machine-checked theorem links

Receipt and verification

First computed	2026-05-17T21:40:25.546025Z
Last reissued	2026-05-17T21:57:18.865043Z
Builder	pith-number-builder-2026-05-17-v1
Signature	unsigned_v0
Schema	pith-number/v1.0

Canonical hash

7a98042f437a4f423ffdbaefd9771ff68b269f25998b6f236e13f39a7620b934

Aliases

arxiv: 2605.15143 · arxiv_version: 2605.15143v1 · pith_short_12: PKMAIL2DPJHU · pith_short_16: PKMAIL2DPJHUEP75 · pith_short_8: PKMAIL2D

Agent API

Resolver JSON Graph JSON Events JSON Schema Signing key

Verify this Pith Number yourself

curl -sH 'Accept: application/ld+json' https://pith.science/pith/PKMAIL2DPJHUEP75XLX5S5Y762 \
  | jq -c '.canonical_record' \
  | python3 -c "import sys,json,hashlib; b=json.dumps(json.loads(sys.stdin.read()), sort_keys=True, separators=(',',':'), ensure_ascii=False).encode(); print(hashlib.sha256(b).hexdigest())"
# expect: 7a98042f437a4f423ffdbaefd9771ff68b269f25998b6f236e13f39a7620b934

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "5dbdde7bc0005cb26ebdc9fa67d906a3e2285e4023686b1c90d0205c94fc4a29",
    "cross_cats_sorted": [
      "cs.PL"
    ],
    "license": "http://creativecommons.org/licenses/by-nc-sa/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-14T17:47:24Z",
    "title_canon_sha256": "d2e81b86f63e65438e4a46be466612d037de109a3a05dae62678aaa9ffabe0da"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.15143",
    "kind": "arxiv",
    "version": 1
  }
}