Pith. sign in

Paper Citation Record · LEDGER

Finding Inductive Loop Invariants using Large Language Models

As of 10 August 2026, this Paper Citation Record lists 0 of 0 outbound references and 18 inbound Pith citation observations for arXiv:2311.07948.

A citation records a reference. It does not transfer a finding from one paper to another.

pith.paper-citation-record.v1
2311.07948 v1

Coverage vector

measured 0 of 0 reference resolution

Typed states for the displayed outbound observations.

Source: paper_references, paper_reference_links

measured 18 of 18 standing notices

One-hop event checks from named stored sources.

Source: scholarly_work_events, retraction_status_cache, observed 2026-08-10T06:31:04.303077+00:00

measured 18 of 18 inbound itemization

Pith citing papers itemized under the disclosed page cap.

Source: paper_references, paper_reference_links, observed 2026-08-09T14:58:50.081241Z

measured 1 of 1 external citation measurements

A source-named dated measurement, never combined with another source.

Source: arxiv_reference, observed 2026-08-05T02:28:24.338817Z

Reference resolution

0 of 0 outbound references displayed

  • verified exact0
  • verified fuzzy0
  • unresolved0
  • parse uncertain0
  • malformed identifier0
  • metadata mismatch0

External citation measurements

15
arxiv_reference, observed 2026-08-05T02:28:24.338817Z

Outbound references

No outbound reference observations are available for this paper version.

Pith citing papers

Observation 1bc8450f-0b71-496f-a4fb-58b50dd4088b · inbound

Next Steps in LLM-Supported Java Verification cites this paper.

Next Steps in LLM-Supported Java Verification Finding Inductive Loop Invariants using Large Language Models

Reference 11

Resolution
unresolved
no resolver link, observed 2026-08-09T14:58:50.081241Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-08-09T14:58:50.081241Z digest=sha256:74082cee79e0373483aad4a5560f5b5f7f76d43de5a9d9631bdfc18aa9b9be64

Observation b77bb270-d6d8-4f8d-a47c-322785756d80 · inbound

RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation cites this paper.

RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation Finding Inductive Loop Invariants using Large Language Models

Reference 8

Resolution
unresolved
no resolver link, observed 2026-08-08T19:47:52.220414Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-08-08T19:47:52.220414Z digest=sha256:8aa05d7100dafd460ff5027b27bf33ea3b15a35569bb77324aaf9afa815378dc

Observation b3775d84-0058-4c7f-9174-08c29e01e1ec · inbound

ClassInvGen: Class Invariant Synthesis using Large Language Models cites this paper.

ClassInvGen: Class Invariant Synthesis using Large Language Models Finding Inductive Loop Invariants using Large Language Models

Reference 19

Resolution
verified exact
arxiv_id, observed 2026-05-23T02:45:19.504615Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-23T02:42:59.190220Z digest=sha256:53017098e8c4d6b2df78775ba2df82ed16c72fad8b751e21cb2dec0cd2a46842

Observation f68b16e1-d3a8-4d32-aac2-bace0fe3595b · inbound

Autoformalization in the Era of Large Language Models: A Survey cites this paper.

Autoformalization in the Era of Large Language Models: A Survey Finding Inductive Loop Invariants using Large Language Models

Reference 22

Resolution
unresolved
no resolver link, observed 2026-08-07T12:49:11.691284Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-08-07T12:49:11.691284Z digest=sha256:d60c35dc2d3a0feea3c4d1ba545b4ddf585c6cedd8958a2e98f9ba9f65a1d2fa

Observation 5bd45359-6966-4579-a488-3ca578eee51a · inbound

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware? cites this paper.

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware? Finding Inductive Loop Invariants using Large Language Models

Reference 20

Resolution
metadata mismatch
arxiv_id, observed 2026-05-18T01:35:36.366509Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-18T01:34:03.866227Z digest=sha256:003333fd8f37a58156042525b399f257b711ce36f21efa7a2328cc361049e090

Observation c6197ca3-cec3-431b-bae3-52bc37f37b92 · inbound

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware? cites this paper.

Large Lemma Miners: Can LLMs do Induction Proofs for Hardware? Finding Inductive Loop Invariants using Large Language Models

Reference 20

Resolution
unresolved
no resolver link, observed 2026-08-04T00:14:49.344571Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-08-04T00:14:49.344571Z digest=sha256:786234a01af8e7260c4cce0088bc95a5649083d566712f246e47148caab2fd30

Observation abf1fe92-39af-4257-afea-54472f3c1604 · inbound

The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee cites this paper.

The 4/$\delta$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee Finding Inductive Loop Invariants using Large Language Models

Reference 86

Resolution
unresolved
no resolver link, observed 2026-08-03T19:22:04.094265Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-08-03T19:22:04.094265Z digest=sha256:0b8770349409d48e13037bf3e40a2143614943116161178765eff3b99ec5eecf

Observation b5fe77ab-26f5-44d2-bfff-81beee2977bd · inbound

Evaluating LLM-Generated ACSL Annotations for Formal Verification cites this paper.

Evaluating LLM-Generated ACSL Annotations for Formal Verification Finding Inductive Loop Invariants using Large Language Models

Reference 11

Resolution
verified exact
arxiv_id, observed 2026-05-15T22:16:42.360262Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-15T22:15:21.599523Z digest=sha256:ff98ec59743e04c2c801d9ceb4dc5c5aa163c8e1ae85a1cb7815846a1a303c21

Observation bf3ba58c-092d-4e30-93ba-cb5e72912f97 · inbound

Verification Modulo Tested Library Contracts cites this paper.

Verification Modulo Tested Library Contracts Finding Inductive Loop Invariants using Large Language Models

Reference 26

Resolution
verified exact
arxiv_id, observed 2026-05-10T08:27:51.708199Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-10T08:26:04.824743Z digest=sha256:21b74123c11ecef1e678ce3c81df020fb2ea6761d965a694932f282f79bb0067

Observation f9428955-2176-4072-a67d-87e2369ee4da · inbound

Verification Modulo Tested Library Contracts cites this paper.

Verification Modulo Tested Library Contracts Finding Inductive Loop Invariants using Large Language Models

Reference 26

Resolution
verified exact
arxiv_id, observed 2026-05-11T04:50:54.767427Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-11T01:03:36.128665Z digest=sha256:bd8b4416768df700aa8643034f5e2c0e3213f9b061b926b4cda72277b789eb8e

Observation 2765da68-cdfe-4f1b-8ed7-42097997e410 · inbound

Combining Mechanical and Agentic Specification Inference for Move cites this paper.

Combining Mechanical and Agentic Specification Inference for Move Finding Inductive Loop Invariants using Large Language Models

Reference 9

Resolution
metadata mismatch
arxiv_id, observed 2026-05-12T07:06:28.026062Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-12T03:46:00.030182Z digest=sha256:331a639d5d1c2f12a879ad97712fc417aab425f8649c6f6268acff86e2641349

Observation a9decb9f-2375-4a35-9692-253bff17ef8c · inbound

Combining Mechanical and Agentic Specification Inference for Move cites this paper.

Combining Mechanical and Agentic Specification Inference for Move Finding Inductive Loop Invariants using Large Language Models

Reference 9

Resolution
metadata mismatch
arxiv_id, observed 2026-05-14T22:08:04.531513Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-14T22:04:25.788782Z digest=sha256:04487ab226c62939fecebd76bb405e195e934f48a748400ed1dfec9266ef4b45

Observation 72361d75-f4e9-4cbe-bbe9-f913f921dbc8 · inbound

Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors cites this paper.

Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors Finding Inductive Loop Invariants using Large Language Models

Reference 20

Resolution
verified exact
arxiv_id, observed 2026-05-20T00:57:54.258467Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-05-20T00:54:59.425270Z digest=sha256:e2760562d9a8c0dd725712af3c59773a38cd5143d58b8ebcb26ce7f410b25722

Observation 04f3ca2a-c30d-4ed5-b70d-7a63f3f60a00 · inbound

Automating Formal Verification with Reinforcement Learning and Recursive Inference cites this paper.

Automating Formal Verification with Reinforcement Learning and Recursive Inference Finding Inductive Loop Invariants using Large Language Models

Reference 88

Resolution
metadata mismatch
arxiv_id, observed 2026-06-28T23:52:49.326627Z

Source-reported events for the cited work

No event found in the named queried sources as of 2026-08-10T06:31:04.303077+00:00.

source=pdf_text observed=2026-06-28T23:52:36.891080Z digest=sha256:d4d729ef7cefd3b9f35efb2aae91a1006ac8ab9b16caa7981c92bfb0c2bb65c6

Observation 7c26dafc-df68-491a-bddd-901ae0ebf1c6 · inbound

InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs cites this paper.

InvWeaver: Deductive Feedback for Invariant Synthesis in Interacting-Loop Programs Finding Inductive Loop Invariants using Large Language Models

Reference 8

Resolution
unresolved
no resolver link, observed 2026-07-11T08:00:14.766840Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-07-11T08:00:14.766840Z digest=sha256:114fe5dd416b40dc4c6e7616387840e6c84999657244c9c9d5ea9d3d7441b5bb

Observation 2e693e9e-6af2-4ebc-bb46-34e9a0a5314a · inbound

Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability cites this paper.

Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability Finding Inductive Loop Invariants using Large Language Models

Reference 10

Resolution
unresolved
no resolver link, observed 2026-07-13T03:34:35.116630Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-07-13T03:34:35.116630Z digest=sha256:f9ac8d6ef69a7e53324a0b95e8c8018e56fe685bad00829e1c690b30e696846f

Observation 0f36d5b9-4412-46ad-8070-12bc3a69d54c · inbound

LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference cites this paper.

LimICE: Integrating LLM into ICE Framework for Efficient Loop Invariant Inference Finding Inductive Loop Invariants using Large Language Models

Reference 22

Resolution
unresolved
no resolver link, observed 2026-08-01T04:51:20.140358Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-08-01T04:51:20.140358Z digest=sha256:976a796f4bdb6066fc045c1541343fd55ed4be7c6cf2ccf6e9fd3deabd9403ef

Observation b63a6b59-2c15-4e3e-b417-3ef1810f7e46 · inbound

VeriSkill: A Self-Evolution Framework for Program Verification Skills cites this paper.

VeriSkill: A Self-Evolution Framework for Program Verification Skills Finding Inductive Loop Invariants using Large Language Models

Reference 2023

Resolution
unresolved
no resolver link, observed 2026-08-01T02:26:35.207539Z

Source-reported events for the cited work

Unavailable: canonical work link unavailable.

source=pdf_text observed=2026-08-01T02:26:35.207539Z digest=sha256:2d92cd39a67fa594708eb02fc6c523887952146a28420f4d4fda457f737eafa4