A new framework synthesizes library method contracts that are adequate for client verification and pass testing scrutiny, using CHC solvers and ICE learning.
Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, and Rahul Sharma
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.
-
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.