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
7 Pith papers cite this work, alongside 15 external citations. Polarity classification is still indexing.
7
Pith papers citing it
15
external citations · external index
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.
ClassInvGen co-generates class invariants and tests with LLMs to outperform pure LLM generation and Daikon on C++ data structures.
RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.
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.
LLMs, verified by a symbolic model checker, produced correct inductive strengthenings for 82 of 94 curated RTL safety properties.
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.
-
Automating Formal Verification with Reinforcement Learning and Recursive Inference
RLVR training raises verified Dafny pass rates from 9.7% to 31.1% on a filtered benchmark while a Lean proof scaffold lifts success from 46.2% to 69.2% on a pilot set and solves 7 of 42 prior unsolved tasks.
-
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.
-
Large Lemma Miners: Can LLMs do Induction Proofs for Hardware?
LLMs, verified by a symbolic model checker, produced correct inductive strengthenings for 82 of 94 curated RTL safety properties.
-
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.