Pith Number

pith:BJJQRWZQ

pith:2026:BJJQRWZQUDSP7G3BNQVIZMIVSM

not attested not anchored not stored refs resolved

Certificate-Aware Property-Directed Reachability

Arman Ferdowsi, Laura Kovacs

A certificate-aware variant of property-directed reachability jointly optimizes runtime, certificate size, and checker time on hardware safety problems.

arxiv:2605.16472 v1 · 2026-05-15 · cs.LO · cs.AR

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

Add to your LaTeX paper

\usepackage{pith}
\pithnumber{BJJQRWZQUDSP7G3BNQVIZMIVSM}

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

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

On the 2024 Hardware Model Checking Competition bit-level safety benchmarks, CAPDR solves six more instances than the baseline. Over each configuration's checker-accepted solved set, the median certificate-size proxy decreases by 24.6% and the median checker time by 49%. Post-fixpoint invariant minimization yields further reductions.

C2weakest assumption

The learned ranking policy over PDR choice points (blocker generalization, obligation ordering, clause pushing) produces the observed joint improvements without introducing any unsoundness, given that every state-changing action remains guarded by the identical SAT checks as standard PDR and final claims are accepted only after independent checker validation.

C3one line summary

CAPDR augments PDR with a learned ranking policy over blocker generalization, obligation ordering, and clause pushing to reduce median certificate size by 24.6% and checker time by 49% while solving six additional 2024 HWMCC bit-level safety instances.

References

34 extracted · 34 resolved · 1 Pith anchors

[1] Sat-based model checking without unrolling, 2011

[2] Introducing certificates to the hardware model checking competition, 2025

[3] Hardware model checking competition 2025, 2025

[4] Improvements in software verification and witness validation: SV-COMP 2025, 2025

[5] Deepic3: Guiding ic3 algorithms by graph neural network clause prediction, 2024

Formal links

1 machine-checked theorem link

Receipt and verification

First computed	2026-05-20T00:02:23.721209Z
Builder	pith-number-builder-2026-05-17-v1
Signature	Pith Ed25519 (`pith-v1-2026-05`) · public key
Schema	pith-number/v1.0

Canonical hash

0a5308db30a0e4ff9b616c2a8cb11593230ac717d6e590a4a9a9550d0482fc29

Aliases

arxiv: 2605.16472 · arxiv_version: 2605.16472v1 · doi: 10.48550/arxiv.2605.16472 · pith_short_12: BJJQRWZQUDSP · pith_short_16: BJJQRWZQUDSP7G3B · pith_short_8: BJJQRWZQ

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/BJJQRWZQUDSP7G3BNQVIZMIVSM \
  | 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: 0a5308db30a0e4ff9b616c2a8cb11593230ac717d6e590a4a9a9550d0482fc29

Canonical record JSON

{
  "metadata": {
    "abstract_canon_sha256": "3b19558e7fdd7f3776b1107fddb653ebe78b981918b8340528dba670f4146530",
    "cross_cats_sorted": [
      "cs.AR"
    ],
    "license": "http://creativecommons.org/licenses/by-nc-nd/4.0/",
    "primary_cat": "cs.LO",
    "submitted_at": "2026-05-15T14:15:33Z",
    "title_canon_sha256": "6c286a11a7971e102713160ba9ca5472edf7be50418ecc197a5695904c8bac65"
  },
  "schema_version": "1.0",
  "source": {
    "id": "2605.16472",
    "kind": "arxiv",
    "version": 1
  }
}