109 citations · 425 across the 36 of their papers we have counts for
22 papers · 1 filter
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…
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…
LLM-Vectorizer: LLM-based Verified Loop Vectorizer
Jubi Taneja, Avery Laird, Cong Yan +2
Vectorization is a powerful optimization technique that significantly boosts the performance of high performance computing applications operating on large data arrays. Despite deca…
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri +2
Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs…
LLM-Based Test-Driven Interactive Code Generation: User Study and Empirical Evaluation
Sarah Fakhoury, Aaditya Naik, Georgios Sakkas +2
Large language models (LLMs) have shown great potential in automating significant aspects of coding by producing natural code from informal natural language (NL) intent. However, g…
Program Structure Aware Precondition Generation
Elizabeth Dinella, Shuvendu Lahiri, Mayur Naik
We introduce a novel approach for inferring natural preconditions from code. Our technique produces preconditions of high quality in terms of both correctness (modulo a test genera…
Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
Madeline Endres, Sarah Fakhoury, Saikat Chakraborty +1
Informal natural language that describes code functionality, such as code comments or function documentation, may contain substantial information about a programs intent. However,…
Towards Generating Functionally Correct Code Edits from Natural Language Issue Descriptions
Sarah Fakhoury, Saikat Chakraborty, Madan Musuvathi +1
Large language models (LLMs), such as OpenAI's Codex, have demonstrated their potential to generate code from natural language descriptions across a wide range of programming tasks…
Interactive Code Generation via Test-Driven User-Intent Formalization
Shuvendu K. Lahiri, Sarah Fakhoury, Aaditya Naik +8
Large language models (LLMs) have shown great potential in automating significant aspects of coding by producing natural code from informal natural language (NL) intent. However, w…
Can Pre-trained Language Models be Used to Resolve Textual and Semantic Merge Conflicts?
Jialu Zhang, Todd Mytkowicz, Mike Kaufman +2
Program merging is standard practice when developers integrate their individual changes to a common code base. When the merge algorithm fails, this is called a merge conflict. The…
Program Merge Conflict Resolution via Neural Transformers
Alexey Svyatkovskiy, Sarah Fakhoury, Negar Ghorbani +6
Collaborative software development is an integral part of the modern software development life cycle, essential to the success of large-scale software projects. When multiple devel…
DeepMerge: Learning to Merge Programs
Elizabeth Dinella, Todd Mytkowicz, Alexey Svyatkovskiy +3
In collaborative software development, program merging is the mechanism to integrate changes from multiple programmers. Merge algorithms in modern version control systems report a…
Can Program Synthesis be Used to Learn Merge Conflict Resolutions? An Empirical Analysis
Rangeet Pan, Vu Le, Nachiappan Nagappan +3
Forking structure is widespread in the open-source repositories and that causes a significant number of merge conflicts. In this paper, we study the problem of textual merge confli…
A Dataset of Dockerfiles
Jordan Henkel, Christian Bird, Shuvendu K. Lahiri +1
Dockerfiles are one of the most prevalent kinds of DevOps artifacts used in industry. Despite their prevalence, there is a lack of sophisticated semantics-aware static analysis of…
Learning from, Understanding, and Supporting DevOps Artifacts for Docker
Jordan Henkel, Christian Bird, Shuvendu K. Lahiri +1
With the growing use of DevOps tools and frameworks, there is an increased need for tools and techniques that support more than code. The current state-of-the-art in static develop…
Enabling Open-World Specification Mining via Unsupervised Learning
Jordan Henkel, Shuvendu K. Lahiri, Ben Liblit +1
Many programming tasks require using both domain-specific code and well-established patterns (such as routines concerned with file IO). Together, several small patterns combine to…
Datalog-based Scalable Semantic Diffing of Concurrent Programs
Chungha Sung, Shuvendu Lahiri, Constantin Enea +1
When an evolving program is modified to address issues related to thread synchronization, there is a need to confirm the change is correct, i.e., it does not introduce unexpected b…
Code Vectors: Understanding Programs Through Embedded Abstracted Symbolic Traces
Jordan Henkel, Shuvendu K. Lahiri, Ben Liblit +1
With the rise of machine learning, there is a great deal of interest in treating programs as data to be fed to learning algorithms. However, programs do not start off in a form tha…
Interprocedural Semantic Change-Impact Analysis using Equivalence Relations
Alex Gyori, Shuvendu K. Lahiri, Nimrod Partush
Change-impact analysis (CIA) is the task of determining the set of program elements impacted by a program change. Precise CIA has great potential to avoid expensive testing and cod…