Citations

@article{pldi2024intrinsic,
author = {Murali, Adithya and Rivera, Cody and Madhusudan, P.},
title = {Predictable Verification using Intrinsic Definitions},
year = {2024},
issue_date = {June 2024},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {8},
number = {PLDI},
url = {https://doi.org/10.1145/3656450},
doi = {10.1145/3656450},
abstract = {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 that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using Boogie and prove a suite of data structure manipulating programs correct.},
journal = {Proc. ACM Program. Lang.},
month = {jun},
articleno = {220},
numpages = {26},
keywords = {Decidability, Ghost-Code Annotations, Intrinsic Definitions, Predictable Verification, Verification of Linked Data Structures}
}

@article{oopsla2023completeness,
author = {Murali, Adithya and Pe\~{n}a, Lucas and Jhala, Ranjit and Madhusudan, P.},
title = {Complete First-Order Reasoning for Properties of Functional Programs},
year = {2023},
issue_date = {October 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {7},
number = {OOPSLA2},
url = {https://doi.org/10.1145/3622835},
doi = {10.1145/3622835},
abstract = {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 definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.},
journal = {Proc. ACM Program. Lang.},
month = {oct},
articleno = {259},
numpages = {30},
keywords = {First-Order Logic, Algebraic Datatypes (ADTs), Refinement Types, Liquid Haskell, Thrifty Instantiation, Natural Proofs, Completeness}
}

@article{framelogictoplas2023,
author = {Murali, Adithya and Pe\~{n}a, Lucas and L\"{o}ding, Christof and Madhusudan, P.},
title = {A First-Order Logic with Frames},
year = {2023},
issue_date = {June 2023},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {45},
number = {2},
issn = {0164-0925},
url = {https://doi.org/10.1145/3583057},
doi = {10.1145/3583057},
abstract = {We propose a novel logic, Frame Logic (FL), that extends first-order logic and recursive definitions with a construct Sp(·) that captures the implicit supports of formulas—the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in frame logic.},
journal = {ACM Trans. Program. Lang. Syst.},
month = {may},
articleno = {7},
numpages = {44},
keywords = {Frame reasoning, program logics, first-order logic with recursive definitions, program verification, first-order logic, heap verification}
}

@article{oopsla2022lemmasynthesis,
author = {Murali, Adithya and Pe\~{n}a, Lucas and Blanchard, Eion and L\"{o}ding, Christof and Madhusudan, P.},
title = {Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints},
year = {2022},
issue_date = {October 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {OOPSLA2},
url = {https://doi.org/10.1145/3563354},
doi = {10.1145/3563354},
abstract = {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 (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not admit even complete procedures. In this paper, we undertake a novel approach for synthesizing inductive hypotheses to prove validity in this logic. The idea is to utilize several kinds of finite first-order models as counterexamples that capture the non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs and demonstrate the effectiveness of our methodology.},
journal = {Proc. ACM Program. Lang.},
month = {oct},
articleno = {191},
numpages = {30},
keywords = {Verifying Linked Data Structures, Learning Logics, First Order Logic with Least Fixpoints, Inductive Hypothesis Synthesis, Counterexample-Guided Inductive Synthesis}
}

@article{oopsla2022axiomsynthesis,
author = {Krogmeier, Paul and Lin, Zhengyao and Murali, Adithya and Madhusudan, P.},
title = {Synthesizing Axiomatizations Using Logic Learning},
year = {2022},
issue_date = {October 2022},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {6},
number = {OOPSLA2},
url = {https://doi.org/10.1145/3563348},
doi = {10.1145/3563348},
abstract = {Axioms and inference rules form the foundation of deductive systems and are crucial in the study of reasoning with logics over structures. Historically, axiomatizations have been discovered manually with much expertise and effort. In this paper we show the feasibility of using synthesis techniques to discover axiomatizations for different classes of structures, and in some contexts, automatically prove their completeness. For evaluation, we apply our technique to find axioms for (1) classes of frames in modal logic characterized in first-order logic and (2) the class of language models with regular operations.},
journal = {Proc. ACM Program. Lang.},
month = {oct},
articleno = {185},
numpages = {29},
keywords = {Inductive Synthesis, Learning Logics, Axiomatization}
}

@inproceedings{ijcai2022visualpuzzles,
  title     = {Composing Neural Learning and Symbolic Reasoning with an Application to Visual Discrimination},
  author    = {Adithya Murali and Atharva Sehgal and Paul Krogmeier and P. Madhusudan},
  booktitle = {Proceedings of the Thirty-First International Joint Conference on
               Artificial Intelligence, {IJCAI-22}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {Luc De Raedt},
  pages     = {3358--3365},
  year      = {2022},
  month     = {7},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2022/466},
  url       = {https://doi.org/10.24963/ijcai.2022/466}
}

@InProceedings{cav2020uninterpretedsynthesis,
author="Krogmeier, Paul
and Mathur, Umang
and Murali, Adithya
and Madhusudan, P.
and Viswanathan, Mahesh",
editor="Lahiri, Shuvendu K.
and Wang, Chao",
title="Decidable Synthesis of Programs with Uninterpreted Functions",
booktitle="Computer Aided Verification",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="634--657",
isbn="978-3-030-53291-8"
}

@InProceedings{esop2020framelogic,
author="Murali, Adithya
and Pe{\~{n}}a, Lucas
and L{\"o}ding, Christof
and Madhusudan, P.",
editor="M{\"u}ller, Peter",
title="A First-Order Logic with Frames",
booktitle="Programming Languages and Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="515--543",
isbn="978-3-030-44914-8"
}

@article{popl2020uninterpretedmemorysafety,
author = {Umang Mathur and Adithya Murali and Paul Krogmeier and P. Madhusudan and Mahesh Viswanathan},
title = {Deciding Memory Safety for Single-Pass Heap-Manipulating Programs},
issue_date = {January 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {POPL},
url = {https://doi.org/10.1145/3371103},
doi = {10.1145/3371103},
journal = {Proc. ACM Program. Lang.},
month = {dec},
articleno = {35},
numpages = {29}
}

@INPROCEEDINGS{fmcad2019kaizen,
author={Faria Kalim and Karl Palmskog and Jayasi Mehar and Adithya Murali and Indranil Gupta and P. Madhusudan},
booktitle={2019 Formal Methods in Computer Aided Design (FMCAD)},
title={Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity},
year={2019},
volume={},
number={},
pages={96-104},
doi={10.23919/FMCAD.2019.8894248}}

@Article{dagstuhl19361report_logic_and_learning,
  author =	{Michael Benedikt and Kristian Kersting and Phokion G. Kolaitis and Daniel Neider},
  title =	{{Logic and Learning (Dagstuhl Seminar 19361)}},
  pages =	{1--22},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Michael Benedikt and Kristian Kersting and Phokion G. Kolaitis and Daniel Neider},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/11842},
  URN =		{urn:nbn:de:0030-drops-118425},
  doi =		{10.4230/DagRep.9.9.1},
  annote =	{Keywords: Artificial Intelligence, Automated reasoning, Databases, Deep Learning, Inductive Logic Programming, Logic, Logic and Learning, Logic for Machine Learning, Logic vs. Machine Learning, Machine Learning, Machine Learning for Logic, Neurosymbolic methods}
}