109 citations · 425 across the 36 of their papers we have counts for
38 papers
Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
Shuvendu K. Lahiri
Formal verification provides the strongest correctness guarantees for software, and verification-aware languages can produce sound, machine-checked proofs. Recent AI coding agents…
Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
Shuvendu K. Lahiri
Agentic AI systems can now generate code with remarkable fluency, but a fundamental question remains: \emph{does the generated code actually do what the user intended?} The gap bet…
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
Chuyue Sun, Yican Sun, Daneshvar Amrollahi +5
We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs…
ClassInvGen: Class Invariant Synthesis using Large Language Models
Chuyue Sun, Viraj Agashe, Saikat Chakraborty +5
Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not on…
Automated Proof Generation for Rust Code via Self-Evolution
Tianyu Chen, Shuai Lu, Shan Lu +11
Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction an…
AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu +10
Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generatio…