11 citations · 33 across the 14 of their papers we have counts for
15 papers
Agents as Software: A Programming Languages Agenda for Agent Reliability
Shraddha Barke, Adithya Murali
AI agents increasingly resemble software systems: they call tools, remember facts, follow policies, delegate work, and take actions with real consequences. % Yet the ``program'' of…
Faithful Autoformalization of Natural Language Assertions
Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali
Formal contracts are essential for software testing and verification, yet writing them remains labor-intensive and error-prone. LLMs offer a promising path toward autoformalization…
Imprompt: A Language Framework for Prompt Programming
Chentian Wu, Shengyuan Yang, Adithya Murali
With the unprecedented success of Language Models (LMs), the science of Prompt Engineering has evolved the powerful idea of Prompt Programming, where prompts are treated as a progr…
Programmers Are Poor and Overconfident Judges of LLM-Generated Assertions
Zhanna Kaufman, Yuriy Brun, Adithya Murali +1
Code comprehension and code review are already critically important software engineering tasks, and the rising use of AI code generation tools is only increasing that importance. G…
Counterexample Guided Learning in the Large using Reasoning Agents
Hongyi Liu, Frederic Sala, Thomas Reps +1
LLMs and LLM agents should improve when given feedback, but identifying when they are able to do so is difficult: feedback is heterogeneous, domain-specific, and difficult to contr…
Complete first-order reasoning for functional programs
Adithya Murali, Lucas Peña, Ranjit Jhala +1
Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function…
Verification Modulo Tested Library Contracts
Abhishek Uppar, Omar Muhammad, Sumanth Prabhu +3
We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate th…
FO-Complete Program Verification for Heap Logics
Adithya Murali, Hrishikesh Balakrishnan, Aaron Councilman +1
We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of FO-completeness is a theoretical guarantee that all…
Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
Neta Elad, Adithya Murali, Sharon Shoham
For over two decades Separation Logic has been arguably the most popular framework for reasoning about heap-manipulating programs, as well as reasoning about shared resources and p…
Predictable Verification using Intrinsic Definitions
Adithya Murali, Cody Rivera, P. Madhusudan
We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show th…
Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
Adithya Murali, Lucas Peña, Eion Blanchard +2
Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (…
Decidable Synthesis of Programs with Uninterpreted Functions
Paul Krogmeier, Umang Mathur, Adithya Murali +2
We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class…
Composing Neural Learning and Symbolic Reasoning with an Application to Visual Discrimination
Adithya Murali, Atharva Sehgal, Paul Krogmeier +1
We consider the problem of combining machine learning models to perform higher-level cognitive tasks with clear specifications. We propose the novel problem of Visual Discriminatio…
Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Umang Mathur, Adithya Murali, Paul Krogmeier +2
We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We…
A First-Order Logic with Frames
Adithya Murali, Lucas Peña, Christof Löding +1
We propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct Sp(.) that captures the implicit supports of formul…