| 2022 | IJCAI | Composing Neural Learning and Symbolic Reasoning with an Application to Visual Discrimination. | Adithya Murali, Atharva Sehgal, Paul Krogmeier, P. Madhusudan |
| 2020 | CAV | Decidable Synthesis of Programs with Uninterpreted Functions. | Paul Krogmeier, Umang Mathur, Adithya Murali, P. Madhusudan, Mahesh Viswanathan |
| 2020 | ESOP | A First-Order Logic with Frames. | Adithya Murali, Lucas Pea, Christof Lding, P. Madhusudan |
| 2020 | TACAS | What's Decidable About Program Verification Modulo Axioms? | Umang Mathur, P. Madhusudan, Mahesh Viswanathan |
| 2019 | FMCAD | Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity. | Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, Indranil Gupta, P. Madhusudan |
| 2019 | PLDI | Learning stateful preconditions modulo a test generator. | Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, Tao Xie |
| 2019 | SAS | Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants. | Daniel Neider, Shambwaditya Saha, Pranav Garg, P. Madhusudan |
| 2018 | CSL | A Decidable Fragment of Second Order Logic With Applications to Synthesis. | P. Madhusudan, Umang Mathur, Shambwaditya Saha, Mahesh Viswanathan |
| 2018 | MFCS | Lagrange's Theorem for Binary Squares. | P. Madhusudan, Dirk Nowotka, Aayush Rajasekaran, Jeffrey O. Shallit |
| 2018 | TACAS | Invariant Synthesis for Incomplete Verification Engines. | Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, Daejun Park |
| 2017 | ICST | Efficient Incrementalized Runtime Checking of Linear Measures on Lists. | Alex Gyori, Pranav Garg, Edgar Pek, P. Madhusudan |
| 2016 | POPL | Learning invariants using decision trees and implication counterexamples. | Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth |
| 2016 | TACAS | Abstract Learning Frameworks for Synthesis. | Christof Lding, P. Madhusudan, Daniel Neider |
| 2016 | TACAS | Synthesizing Piece-Wise Functions by Learning Classifiers. | Daniel Neider, Shambwaditya Saha, P. Madhusudan |
| 2015 | CAV | Alchemist: Learning Guarded Affine Functions. | Shambwaditya Saha, Pranav Garg, P. Madhusudan |
| 2014 | CAV | ICE: A Robust Framework for Learning Invariants. | Pranav Garg, Christof Lding, P. Madhusudan, Daniel Neider |
| 2014 | CAV | Vac - Verifier of Administrative Role-Based Access Control Policies. | Anna Lisa Ferrara, P. Madhusudan, Truc L. Nguyen, Gennaro Parlato |
| 2014 | OOPSLA | Natural proofs for asynchronous programs using almost-synchronous reductions. | Ankush Desai, Pranav Garg, P. Madhusudan |
| 2014 | PLDI | Explicit and symbolic techniques for fast and scalable points-to analysis. | Edgar Pek, P. Madhusudan |
| 2014 | PLDI | Natural proofs for data structure manipulation in C using separation logic. | Edgar Pek, Xiaokang Qiu, P. Madhusudan |
| 2013 | CAV | Learning Universally Quantified Invariants of Linear Data Structures. | Pranav Garg, Christof Lding, P. Madhusudan, Daniel Neider |
| 2013 | SAS | Quantified Data Automata on Skinny Trees: An Abstract Domain for Lists. | Pranav Garg, P. Madhusudan, Gennaro Parlato |
| 2013 | TACAS | Policy Analysis for Self-administrated Role-Based Access Control. | Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato |
| 2012 | TACAS | Reachability under Contextual Locking. | Rohit Chadha, P. Madhusudan, Mahesh Viswanathan |
| 2011 | POPL | The tree width of auxiliary storage. | P. Madhusudan, Gennaro Parlato |
| 2011 | POPL | Decidable logics combining heap structures and data. | P. Madhusudan, Gennaro Parlato, Xiaokang Qiu |
| 2011 | PPoPP | Thread contracts for safe parallelism. | Rajesh K. Karmani, P. Madhusudan, Brandon M. Moore |
| 2011 | SAS | Efficient Decision Procedures for Heaps Using STRAND. | P. Madhusudan, Xiaokang Qiu |
| 2011 | TACAS | Compositionality Entails Sequentializability. | Pranav Garg, P. Madhusudan |
| 2010 | CAV | Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2009 | CAV | Meta-analysis for Atomicity Violations under Nested Locking. | Azadeh Farzan, P. Madhusudan, Francesco Sorrentino |
| 2009 | CAV | Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2009 | MFCS | Query Automata for Nested Words. | P. Madhusudan, Mahesh Viswanathan |
| 2009 | TACAS | The Complexity of Predicting Atomicity Violations. | Azadeh Farzan, P. Madhusudan |
| 2008 | CAV | Monitoring Atomicity in Concurrent Programs. | Azadeh Farzan, P. Madhusudan |
| 2008 | CCS | A formal framework for reflective database access control policies. | Lars E. Olson, Carl A. Gunter, P. Madhusudan |
| 2008 | CSL | An Infinite Automaton Characterization of Double Exponential Time. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2008 | TACAS | Context-Bounded Analysis of Concurrent Queue Systems. | Salvatore La Torre, P. Madhusudan, Gennaro Parlato |
| 2007 | CCS | CANDID: preventing sql injection attacks using dynamic candidate evaluations. | Sruthi Bandhakavi, Prithvi Bisht, P. Madhusudan, V. N. Venkatakrishnan |
| 2007 | WWW | Visibly pushdown automata for streaming XML. | Viraj Kumar, P. Madhusudan, Mahesh Viswanathan |
| 2007 | TACAS | Causal Dataflow Analysis for Concurrent Programs. | Azadeh Farzan, P. Madhusudan |
| 2007 | VMCAI | Learning Algorithms and Formal Verification (Invited Tutorial). | P. Madhusudan |
| 2006 | CAV | Languages of Nested Trees. | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
| 2006 | CAV | Causal Atomicity. | Azadeh Farzan, P. Madhusudan |
| 2006 | CONCUR | Minimization, Learning, and Conformance Testing of Boolean Programs. | Viraj Kumar, P. Madhusudan, Mahesh Viswanathan |
| 2006 | DLT | Adding Nesting Structure to Words. | Rajeev Alur, P. Madhusudan |
| 2006 | POPL | A fixpoint calculus for local and global program flows. | Rajeev Alur, Swarat Chaudhuri, P. Madhusudan |
| 2005 | CAV | Symbolic Compositional Verification by Learning Assumptions. | Rajeev Alur, P. Madhusudan, Wonhong Nam |
| 2005 | ICALP | Congruences for Visibly Pushdown Languages. | Rajeev Alur, Viraj Kumar, P. Madhusudan, Mahesh Viswanathan |
| 2005 | POPL | Synthesis of interface specifications for Java classes. | Rajeev Alur, Pavol Cern, P. Madhusudan, Wonhong Nam |
| 2005 | TACAS | On-the-Fly Reachability and Cycle Detection for Recursive State Machines. | Rajeev Alur, Swarat Chaudhuri, Kousha Etessami, P. Madhusudan |
| 2004 | ICALP | Optimal Reachability for Weighted Timed Games. | Rajeev Alur, Mikhail Bernadsky, P. Madhusudan |
| 2004 | STOC | Visibly pushdown languages. | Rajeev Alur, P. Madhusudan |
| 2004 | TACAS | A Temporal Logic of Nested Calls and Returns. | Rajeev Alur, Kousha Etessami, P. Madhusudan |
| 2003 | CAV | Modular Strategies for Infinite Games on Recursive Graphs. | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2003 | CAV | Timed Control with Partial Observability. | Patricia Bouyer, Deepak D'Souza, P. Madhusudan, Antoine Petit |
| 2003 | CONCUR | Playing Games with Boxes and Diamonds. | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2003 | LICS | Model-checking Trace Event Structures. | P. Madhusudan |
| 2003 | TACAS | Modular Strategies for Recursive Game Graphs. | Rajeev Alur, Salvatore La Torre, P. Madhusudan |
| 2002 | CONCUR | A Decidable Class of Asynchronous Distributed Controllers. | P. Madhusudan, P. S. Thiagarajan |
| 2002 | STACS | Timed Control Synthesis for External Specifications. | Deepak D'Souza, P. Madhusudan |
| 2001 | ICALP | Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs. | P. Madhusudan |
| 2001 | ICALP | Distributed Controller Synthesis for Local Specifications. | P. Madhusudan, P. S. Thiagarajan |
| 2000 | CONCUR | Open Systems in Reactive Environments: Control and Synthesis. | Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, Moshe Y. Vardi |
| 1998 | CONCUR | Controllers for Discrete Event Systems via Morphisms. | P. Madhusudan, P. S. Thiagarajan |