A Categorical Interpretation of Landin's Correspondence Principle. - Anindya Banerjee 001; David A. Schmidt (MFPS, 1993)

A Modular, Polyvariant, and Type-Based Closure Analysis. - Anindya Banerjee 001 (ICFP, 1997)

Stackability in the Simply-Typed Call-by-Value lambda Calculus. - Anindya Banerjee 001; David A. Schmidt (Sci. Comput. Program., 1998)

Region Analysis and the Polymorphic Lambda Calculus. - Anindya Banerjee 001; Nevin Heintze; Jon G. Riecke (LICS, 1999)

A Core Calculus of Dependency. - Martín Abadi; Anindya Banerjee 001; Nevin Heintze; Jon G. Riecke (POPL, 1999)

Design and Correctness of Program Transformations Based on Control-Flow Analysis. - Anindya Banerjee 001; Nevin Heintze; Jon G. Riecke (TACS, 2001)

Secure Information Flow and Pointer Confinement in a Java-like Language. - Anindya Banerjee 001; David A. Naumann (CSFW, 2002)

Representation independence, confinement and access control [extended abstract]. - Anindya Banerjee 001; David A. Naumann (POPL, 2002)

Using Access Control for Secure Information Flow in a Java-like Language. - Anindya Banerjee 001; David A. Naumann (CSFW, 2003)

03411 Final Report - Language Based Security. - Anindya Banerjee 001; Heiko Mantel; David A. Naumann; Andrei Sabelfeld (Language Based Security, 2003)

03411 Abstracts Collection - Language Based Security. - Anindya Banerjee 001; Heiko Mantel; David A. Naumann; Andrei Sabelfeld (Language Based Security, 2003)

Modular Control-Flow Analysis with Rank 2 Intersection Types. - Anindya Banerjee 001; Thomas P. Jensen (Math. Struct. Comput. Sci., 2003)

History-Based Access Control and Secure Information Flow. - Anindya Banerjee 001; David A. Naumann (CASSIS, 2004)

Information Flow Analysis in Logical Form. - Torben Amtoft; Anindya Banerjee 001 (SAS, 2004)

Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. - Qi Sun; Anindya Banerjee 001; David A. Naumann (SAS, 2004)

State Based Ownership, Reentrance, and Encapsulation. - Anindya Banerjee 001; David A. Naumann (ECOOP, 2005)

Ownership confinement ensures representation independence for object-oriented programs. - Anindya Banerjee 001; David A. Naumann (J. ACM, 2005)

Stack-based access control and secure information flow. - Anindya Banerjee 001; David A. Naumann (J. Funct. Program., 2005)

Automata-Based Confidentiality Monitoring. - Gurvan Le Guernic; Anindya Banerjee 001; Thomas P. Jensen; David A. Schmidt (ASIAN, 2006)

A logic for information flow in object-oriented programs. - Torben Amtoft; Sruthi Bandhakavi; Anindya Banerjee 001 (POPL, 2006)

Verification condition generation for conditional information flow. - Torben Amtoft; Anindya Banerjee 001 (FMSE, 2007)

Towards a logical account of declassification. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (PLAS, 2007)

Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. - Marco Pistoia; Anindya Banerjee 001; David A. Naumann (S&P, 2007)

What You Lose is What You Leak: Information Leakage in Declassification Policies. - Anindya Banerjee 001; Roberto Giacobazzi; Isabella Mastroeni (MFPS, 2007)

A logic for information flow analysis with an application to forward slicing of simple imperative programs. - Torben Amtoft; Anindya Banerjee 001 (Sci. Comput. Program., 2007)

A new foundation for control dependence and slicing for modern program structures. - Venkatesh Prasad Ranganath; Torben Amtoft; Anindya Banerjee 001; John Hatcliff; Matthew B. Dwyer (ACM Trans. Program. Lang. Syst., 2007)

Regional Logic for Local Reasoning about Global Invariants. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (ECOOP, 2008)

Formal Techniques for Java-Like Programs. - Elvira Albert; Anindya Banerjee 001; Sophia Drossopoulou; Marieke Huisman; Atsushi Igarashi; Gary T. Leavens; Peter Müller 001; Tobias Wrigstad (ECOOP Workshops, 2008)

Expressive Declassification Policies and Modular Static Enforcement. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (SP, 2008)

Boogie Meets Regions: A Verification Experience Report. - Anindya Banerjee 001; Michael Barnett 001; David A. Naumann (VSTTE, 2008)

Semantics and Enforcement of Expressive Information Flow Policies. - Anindya Banerjee 001 (Formal Aspects in Security and Trust, 2009)

Merlin: specification inference for explicit information flow problems. - V. Benjamin Livshits; Aditya V. Nori; Sriram K. Rajamani; Anindya Banerjee 001 (PLDI, 2009)

A language for information flow: dynamic tracking in multiple interdependent dimensions. - Avraham Shinnar; Marco Pistoia; Anindya Banerjee 001 (PLAS, 2009)

Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. - David A. Naumann; Anindya Banerjee 001 (ESOP, 2010)

Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. - Stan Rosenberg; Anindya Banerjee 001; David A. Naumann (VSTTE, 2010)

Modular Verification of Object-Based Programs - Abstract of Invited Talk. - Anindya Banerjee 001 (FoVeOOS, 2011)

Verification of Information Flow and Access Control Policies with Dependent Types. - Aleksandar Nanevski; Anindya Banerjee 001; Deepak Garg 001 (IEEE Symposium on Security and Privacy, 2011)

Modelling declassification policies using abstract domain completeness. - Isabella Mastroeni; Anindya Banerjee 001 (Math. Struct. Comput. Sci., 2011)

Programming Paradigm Driven Heap Analysis. - Mark Marron; Ondrej Lhoták; Anindya Banerjee 001 (CC, 2012)

Verification of software barriers. - Alexander Malkis; Anindya Banerjee 001 (PPoPP, 2012)

Decision Procedures for Region Logic. - Stan Rosenberg; Anindya Banerjee 001; David A. Naumann (VMCAI, 2012)

Effectively-Propositional Reasoning about Reachability in Linked Data Structures. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Aleksandar Nanevski; Mooly Sagiv (CAV, 2013)

Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. - Gordon Stewart 001; Anindya Banerjee 001; Aleksandar Nanevski (PPDP, 2013)

A Simple Semantics and Static Analysis for Stack Inspection. - Anindya Banerjee 001; David A. Naumann (Festschrift for Dave Schmidt, 2013)

Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. - Anindya Banerjee 001; David A. Naumann (J. ACM, 2013)

Local Reasoning for Global Invariants, Part I: Region Logic. - Anindya Banerjee 001; David A. Naumann; Stan Rosenberg (J. ACM, 2013)

Dependent Type Theory for Verification of Information Flow and Access Control Policies. - Aleksandar Nanevski; Anindya Banerjee 001; Deepak Garg 001 (ACM Trans. Program. Lang. Syst., 2013)

State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings. - Anindya Banerjee 001; David A. Naumann (Aliasing in Object-Oriented Programming, 2013)

Modular reasoning about heap paths via effectively propositional formulas. - Shachar Itzhaky; Anindya Banerjee 001; Neil Immerman; Ori Lahav 001; Aleksandar Nanevski; Mooly Sagiv (POPL, 2014)

A Logical Analysis of Framing for Specifications with Pure Method Calls. - Anindya Banerjee 001; David A. Naumann (VSTTE, 2014)

On Automation in the Verification of Software Barriers: Experience Report. - Alexander Malkis; Anindya Banerjee 001 (J. Autom. Reason., 2014)

Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. - Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (ESOP, 2015)

Mechanized verification of fine-grained concurrent programs. - Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (PLDI, 2015)

A Theory of Slicing for Probabilistic Control Flow Graphs. - Torben Amtoft; Anindya Banerjee 001 (FoSSaCS, 2016)

Relational Logic with Framing and Hypotheses. - Anindya Banerjee 001; David A. Naumann; Mohammad Nikouei (FSTTCS, 2016)

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. - Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco (OOPSLA, 2016)

Relational Logic with Framing and Hypotheses: Technical Report. - Anindya Banerjee 001; David A. Naumann; Mohammad Nikouei (CoRR, 2016)

Concurrent Data Structures Linked in Time. - Germán Andrés Delbianco; Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (ECOOP, 2017)

Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources. - Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco (CoRR, 2017)

A Semantics for Probabilistic Control-Flow Graphs. - Torben Amtoft; Anindya Banerjee 001 (CoRR, 2017)

Concurrent Data Structures Linked in Time (Artifact). - Germán Andrés Delbianco; Ilya Sergey; Aleksandar Nanevski; Anindya Banerjee 001 (Dagstuhl Artifacts Ser., 2017)

A Logical Analysis of Framing for Specifications with Pure Method Calls. - Anindya Banerjee 001; David A. Naumann; Mohammad Nikouei (ACM Trans. Program. Lang. Syst., 2018)

Data Abstraction and Relational Program Logic. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann; Mohammad Nikouei (CoRR, 2019)

Specifying concurrent programs in separation logic: morphisms and simulations. - Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco; Ignacio Fábregas (Proc. ACM Program. Lang., 2019)

Verification of ML Systems via Reparameterization. - Jean-Baptiste Tristan; Joseph Tassarotti; Koundinya Vajjha; Michael L. Wick; Anindya Banerjee 001 (CoRR, 2020)

A Theory of Slicing for Imperative Probabilistic Programs. - Torben Amtoft; Anindya Banerjee 001 (ACM Trans. Program. Lang. Syst., 2020)

A formal proof of PAC learnability for decision stumps. - Joseph Tassarotti; Koundinya Vajjha; Anindya Banerjee 001; Jean-Baptiste Tristan (CPP, 2021)

Navigating the Seismic Shift of Post-Moore Computer Systems Design. - Anindya Banerjee 001; Sankar Basu; Erik Brunvand; Pinaki Mazumder; Rance Cleaveland; Gurdip Singh; Margaret Martonosi; Fernanda Pembleton (IEEE Micro, 2021)

On algebraic abstractions for concurrent separation logics. - Frantisek Farka; Aleksandar Nanevski; Anindya Banerjee 001; Germán Andrés Delbianco; Ignacio Fábregas (Proc. ACM Program. Lang., 2021)

Making Relational Hoare Logic Alignment Complete. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann (CoRR, 2022)

A Relational Program Logic with Data Abstraction and Dynamic Framing. - Anindya Banerjee 001; Ramana Nagasamudram; David A. Naumann; Mohammad Nikouei (ACM Trans. Program. Lang. Syst., 2022)

The WhyRel Prototype for Modular Relational Verification of Pointer Programs. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (TACAS (2), 2023)

Inductive Reasoning for Coinductive Types. - Alexander Bagnall; Gordon Stewart 001; Anindya Banerjee 001 (CoRR, 2023)

The WhyRel Prototype for Relational Verification. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (CoRR, 2023)

Alignment complete relational Hoare logics for some and all. - Ramana Nagasamudram; Anindya Banerjee 001; David A. Naumann (CoRR, 2023)

Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning. - Alexander Bagnall; Gordon Stewart 001; Anindya Banerjee 001 (Proc. ACM Program. Lang., 2023)

A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs. - Torben Amtoft; Anindya Banerjee 001 (CoRR, 2024)