109 citations · 159 across the 10 of their papers we have counts for
10 papers
LLM For Loop Invariant Generation and Fixing: How Far Are We?
Mostafijur Rahman Akhond, Saikat Chakraborty, Gias Uddin
A loop invariant is a property of a loop that remains true before and after each execution of the loop. The identification of loop invariants is a critical step to support automate…
Teaching an Old LLM Secure Coding: Localized Preference Optimization on Distilled Preferences
Mohammad Saqib Hasan, Saikat Chakraborty, Santu Karmaker +1
LLM generated code often contains security issues. We address two key challenges in improving secure code generation. First, obtaining high quality training data covering a broad s…
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…
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat +4
Proof-oriented programs mix computational content with proofs of program correctness. However, the human effort involved in programming and proving is still substantial, despite th…
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…
Studying LLM Performance on Closed- and Open-source Data
Toufique Ahmed, Christian Bird, Premkumar Devanbu +1
Large Language models (LLMs) are finding wide use in software engineering practice. These models are extremely data-hungry, and are largely trained on open-source (OSS) code distri…
Finding Inductive Loop Invariants using Large Language Models
Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty +6
Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become u…
Ranking LLM-Generated Loop Invariants for Program Verification
Saikat Chakraborty, Shuvendu K. Lahiri, Sarah Fakhoury +6
Synthesizing inductive loop invariants is fundamental to automating program verification. In this work, we observe that Large Language Models (such as gpt-3.5 or gpt-4) are capable…
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,…
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…