| 2023 | TACAS | The WhyRel Prototype for Modular Relational Verification of Pointer Programs. | Ramana Nagasamudram, Anindya Banerjee, David A. Naumann |
| 2021 | CPP | A formal proof of PAC learnability for decision stumps. | Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan |
| 2017 | ECOOP | Concurrent Data Structures Linked in Time. | Germn Andrs Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2016 | FOSSACS | A Theory of Slicing for Probabilistic Control Flow Graphs. | Torben Amtoft, Anindya Banerjee |
| 2016 | OOPSLA | Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germn Andrs Delbianco |
| 2015 | ESOP | Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2015 | PLDI | Mechanized verification of fine-grained concurrent programs. | Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee |
| 2014 | POPL | Modular reasoning about heap paths via effectively propositional formulas. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | CAV | Effectively-Propositional Reasoning about Reachability in Linked Data Structures. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv |
| 2013 | PPDP | Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. | Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski |
| 2012 | CC | Programming Paradigm Driven Heap Analysis. | Mark Marron, Ondrej Lhotk, Anindya Banerjee |
| 2012 | PPoPP | Verification of software barriers. | Alexander Malkis, Anindya Banerjee |
| 2012 | VMCAI | Decision Procedures for Region Logic. | Stan Rosenberg, Anindya Banerjee, David A. Naumann |
| 2011 | SP | Verification of Information Flow and Access Control Policies with Dependent Types. | Aleksandar Nanevski, Anindya Banerjee, Deepak Garg |
| 2010 | ESOP | Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. | David A. Naumann, Anindya Banerjee |
| 2009 | ICDCN | Guaranteeing Eventual Coherency across Data Copies, in a Highly Available Peer-to-Peer Distributed File System. | BijayaLaxmi Nanda, Anindya Banerjee, Navin Kabra |
| 2009 | PLDI | Merlin: specification inference for explicit information flow problems. | V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee |
| 2009 | PLDI | A language for information flow: dynamic tracking in multiple interdependent dimensions. | Avraham Shinnar, Marco Pistoia, Anindya Banerjee |
| 2008 | ECOOP | Regional Logic for Local Reasoning about Global Invariants. | Anindya Banerjee, David A. Naumann, Stan Rosenberg |
| 2008 | SP | Expressive Declassification Policies and Modular Static Enforcement. | Anindya Banerjee, David A. Naumann, Stan Rosenberg |
| 2007 | CCS | Verification condition generation for conditional information flow. | Torben Amtoft, Anindya Banerjee |
| 2007 | PLDI | Towards a logical account of declassification. | Anindya Banerjee, David A. Naumann, Stan Rosenberg |
| 2007 | SP | Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. | Marco Pistoia, Anindya Banerjee, David A. Naumann |
| 2006 | POPL | A logic for information flow in object-oriented programs. | Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee |
| 2005 | ECOOP | State Based Ownership, Reentrance, and Encapsulation. | Anindya Banerjee, David A. Naumann |
| 2005 | ESOP | A New Foundation for Control-Dependence and Slicing for Modern Program Structures. | Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff |
| 2004 | SAS | Information Flow Analysis in Logical Form. | Torben Amtoft, Anindya Banerjee |
| 2004 | SAS | Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. | Qi Sun, Anindya Banerjee, David A. Naumann |
| 2002 | POPL | Representation independence, confinement and access control [extended abstract]. | Anindya Banerjee, David A. Naumann |
| 1999 | LICS | Region Analysis and the Polymorphic Lambda Calculus. | Anindya Banerjee, Nevin Heintze, Jon G. Riecke |
| 1999 | POPL | A Core Calculus of Dependency. | Martn Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke |
| 1997 | ICFP | A Modular, Polyvariant, and Type-Based Closure Analysis. | Anindya Banerjee |
| 1994 | SAS | Stackability in the Simply-Typed Call-by-Value Lambda Calculus. | Anindya Banerjee, David A. Schmidt |
| 1993 | MFPS | A Categorical Interpretation of Landin's Correspondence Principle. | Anindya Banerjee, David A. Schmidt |