A new framework synthesizes library method contracts that are adequate for client verification and pass testing scrutiny, using CHC solvers and ICE learning.
Finding inductive loop invariants using large language models
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
representative citing papers
LORIS detects local reasoning errors in LLM-generated proofs for loop invariants by translating natural-language steps to first-order logic implications and using invalid implications to refine the invariants, achieving 93.1% success on 460 C programs.
A neurosymbolic method using two LLM prompting frameworks generates provably correct inductive arguments for 84% of a set of mid-size open-source RTL hardware designs.
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
A hybrid tool pairs mechanical weakest-precondition analysis with an AI agent to infer verifiable specifications for Move programs, using the prover as an oracle to refine results until they pass.
Rule-based annotation generation for ACSL outperforms LLM-based methods in achieving successful formal verification of C programs.
citing papers explorer
-
Verification Modulo Tested Library Contracts
A new framework synthesizes library method contracts that are adequate for client verification and pass testing scrutiny, using CHC solvers and ICE learning.
-
Guiding LLM-based Loop Invariant Synthesis via Feedback on Local Reasoning Errors
LORIS detects local reasoning errors in LLM-generated proofs for loop invariants by translating natural-language steps to first-order logic implications and using invalid implications to refine the invariants, achieving 93.1% success on 460 C programs.
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
A neurosymbolic method using two LLM prompting frameworks generates provably correct inductive arguments for 84% of a set of mid-size open-source RTL hardware designs.
-
ClassInvGen: Class Invariant Synthesis using Large Language Models
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
-
Combining Mechanical and Agentic Specification Inference for Move
A hybrid tool pairs mechanical weakest-precondition analysis with an AI agent to infer verifiable specifications for Move programs, using the prover as an oracle to refine results until they pass.
-
Evaluating LLM-Generated ACSL Annotations for Formal Verification
Rule-based annotation generation for ACSL outperforms LLM-based methods in achieving successful formal verification of C programs.