Anindya Banerjee

Publication Activity (10 Years)

Years Active: 1993-2023
Publications (10 Years): 28

Top Topics

Inductive Reasoning

Decision Stumps

Concurrent Programs

Top Venues

ACM Trans. Program. Lang. Syst.

Proc. ACM Program. Lang.

Publications

Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
The WhyRel Prototype for Relational Verification. CoRR (2023)
Alexander Bagnall, Gordon Stewart, Anindya Banerjee
Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
The WhyRel Prototype for Modular Relational Verification of Pointer Programs. TACAS (2) (2023)
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
Alignment complete relational Hoare logics for some and all. CoRR (2023)
Alexander Bagnall, Gordon Stewart, Anindya Banerjee
Inductive Reasoning for Coinductive Types. CoRR (2023)
Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, Mohammad Nikouei
A Relational Program Logic with Data Abstraction and Dynamic Framing. ACM Trans. Program. Lang. Syst. 44 (4) (2022)
Anindya Banerjee, Ramana Nagasamudram, David A. Naumann
Making Relational Hoare Logic Alignment Complete. CoRR (2022)
Alexander Bagnall, Gordon Stewart, Anindya Banerjee
Formally Verified Samplers From Probabilistic Programs With Loops and Conditioning. CoRR (2022)
Anindya Banerjee, Sankar Basu, Erik Brunvand, Pinaki Mazumder, Rance Cleaveland, Gurdip Singh, Margaret Martonosi, Fernanda Pembleton
Navigating the Seismic Shift of Post-Moore Computer Systems Design. IEEE Micro 41 (6) (2021)
Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan
A formal proof of PAC learnability for decision stumps. CPP (2021)
Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
On algebraic abstractions for concurrent separation logics. Proc. ACM Program. Lang. 5 (POPL) (2021)
Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
On Algebraic Abstractions for Concurrent Separation Logics. CoRR (2020)
Torben Amtoft, Anindya Banerjee
A Theory of Slicing for Imperative Probabilistic Programs. ACM Trans. Program. Lang. Syst. 42 (2) (2020)
Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, Anindya Banerjee
Verification of ML Systems via Reparameterization. CoRR (2020)
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
Specifying concurrent programs in separation logic: morphisms and simulations. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. CoRR (2019)
Mohammad Nikouei, Anindya Banerjee, David A. Naumann
Data Abstraction and Relational Program Logic. CoRR (2019)
Anindya Banerjee, David A. Naumann, Mohammad Nikouei
A Logical Analysis of Framing for Specifications with Pure Method Calls. ACM Trans. Program. Lang. Syst. 40 (2) (2018)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time (Artifact). Dagstuhl Artifacts Ser. 3 (2) (2017)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time. ECOOP (2017)
Torben Amtoft, Anindya Banerjee
A Semantics for Probabilistic Control-Flow Graphs. CoRR (2017)
Torben Amtoft, Anindya Banerjee
A Theory of Slicing for Probabilistic Control-Flow Graphs. CoRR (2017)
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources. CoRR (2017)
Anindya Banerjee, David A. Naumann, Mohammad Nikouei
Relational Logic with Framing and Hypotheses: Technical Report. CoRR (2016)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. OOPSLA (2016)
Torben Amtoft, Anindya Banerjee
A Theory of Slicing for Probabilistic Control Flow Graphs. FoSSaCS (2016)
Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Concurrent Data Structures Linked in Time. CoRR (2016)
Anindya Banerjee, David A. Naumann, Mohammad Nikouei
Relational Logic with Framing and Hypotheses. FSTTCS (2016)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. CoRR (2015)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP (2015)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Mechanized verification of fine-grained concurrent programs. PLDI (2015)
Anindya Banerjee, David A. Naumann
A Logical Analysis of Framing for Specifications with Pure Method Calls. VSTTE (2014)
Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. CoRR (2014)
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv
Modular reasoning about heap paths via effectively propositional formulas. POPL (2014)
Alexander Malkis, Anindya Banerjee
On Automation in the Verification of Software Barriers: Experience Report. J. Autom. Reason. 52 (3) (2014)
Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV (2013)
Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. PPDP (2013)
Anindya Banerjee, David A. Naumann
A Simple Semantics and Static Analysis for Stack Inspection. Festschrift for Dave Schmidt (2013)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Local Reasoning for Global Invariants, Part I: Region Logic. J. ACM 60 (3) (2013)
Anindya Banerjee, David A. Naumann
Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. J. ACM 60 (3) (2013)
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
Dependent Type Theory for Verification of Information Flow and Access Control Policies. ACM Trans. Program. Lang. Syst. 35 (2) (2013)
Stan Rosenberg, Anindya Banerjee, David A. Naumann
Decision Procedures for Region Logic. VMCAI (2012)
Alexander Malkis, Anindya Banerjee
Verification of software barriers. PPOPP (2012)
Mark Marron, Ondrej Lhoták, Anindya Banerjee
Programming Paradigm Driven Heap Analysis. CC (2012)
Anindya Banerjee
Modular Verification of Object-Based Programs - Abstract of Invited Talk. FoVeOOS (2011)
Isabella Mastroeni, Anindya Banerjee
Modelling declassification policies using abstract domain completeness. Math. Struct. Comput. Sci. 21 (6) (2011)
Aleksandar Nanevski, Anindya Banerjee, Deepak Garg
Verification of Information Flow and Access Control Policies with Dependent Types. IEEE Symposium on Security and Privacy (2011)
David A. Naumann, Anindya Banerjee
Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. ESOP (2010)
Stan Rosenberg, Anindya Banerjee, David A. Naumann
Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. VSTTE (2010)
V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee
Merlin: specification inference for explicit information flow problems. PLDI (2009)
Anindya Banerjee
Semantics and Enforcement of Expressive Information Flow Policies. Formal Aspects in Security and Trust (2009)
Avraham Shinnar, Marco Pistoia, Anindya Banerjee
A language for information flow: dynamic tracking in multiple interdependent dimensions. PLAS (2009)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Expressive Declassification Policies and Modular Static Enforcement. IEEE Symposium on Security and Privacy (2008)
Anindya Banerjee, Michael Barnett, David A. Naumann
Boogie Meets Regions: A Verification Experience Report. VSTTE (2008)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Regional Logic for Local Reasoning about Global Invariants. ECOOP (2008)
Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary T. Leavens, Peter Müller, Tobias Wrigstad
Formal Techniques for Java-Like Programs. ECOOP Workshops (2008)
Torben Amtoft, Anindya Banerjee
A logic for information flow analysis with an application to forward slicing of simple imperative programs. Sci. Comput. Program. 64 (1) (2007)
Marco Pistoia, Anindya Banerjee, David A. Naumann
Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. IEEE Symposium on Security and Privacy (2007)
Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, John Hatcliff, Matthew B. Dwyer
A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst. 29 (5) (2007)
Anindya Banerjee, Roberto Giacobazzi, Isabella Mastroeni
What You Lose is What You Leak: Information Leakage in Declassification Policies. MFPS (2007)
Anindya Banerjee, David A. Naumann, Stan Rosenberg
Towards a logical account of declassification. PLAS (2007)
Torben Amtoft, Anindya Banerjee
Verification condition generation for conditional information flow. FMSE (2007)
Gurvan Le Guernic, Anindya Banerjee, Thomas P. Jensen, David A. Schmidt
Automata-Based Confidentiality Monitoring. ASIAN (2006)
Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee
A logic for information flow in object-oriented programs. POPL (2006)
Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer, John Hatcliff
A New Foundation for Control-Dependence and Slicing for Modern Program Structures. ESOP (2005)
Anindya Banerjee, David A. Naumann
State Based Ownership, Reentrance, and Encapsulation. ECOOP (2005)
Anindya Banerjee, David A. Naumann
Stack-based access control and secure information flow. J. Funct. Program. 15 (2) (2005)
Anindya Banerjee, David A. Naumann
Ownership confinement ensures representation independence for object-oriented programs. J. ACM 52 (6) (2005)
Torben Amtoft, Anindya Banerjee
Information Flow Analysis in Logical Form. SAS (2004)
Anindya Banerjee, David A. Naumann
History-Based Access Control and Secure Information Flow. CASSIS (2004)
Qi Sun, Anindya Banerjee, David A. Naumann
Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. SAS (2004)
Anindya Banerjee, David A. Naumann
Using Access Control for Secure Information Flow in a Java-like Language. CSFW (2003)
Anindya Banerjee, Thomas P. Jensen
Modular Control-Flow Analysis with Rank 2 Intersection Types. Math. Struct. Comput. Sci. 13 (1) (2003)
Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld
03411 Abstracts Collection - Language Based Security. Language Based Security (2003)
Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld
03411 Final Report - Language Based Security. Language Based Security (2003)
Anindya Banerjee, David A. Naumann
Ownership Confinement Ensures Representation Independence for Object-Oriented Programs CoRR (2002)
Anindya Banerjee, David A. Naumann
Secure Information Flow and Pointer Confinement in a Java-like Language. CSFW (2002)
Anindya Banerjee, David A. Naumann
Representation independence, confinement and access control [extended abstract]. POPL (2002)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Design and Correctness of Program Transformations Based on Control-Flow Analysis. TACS (2001)
Martín Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke
A Core Calculus of Dependency. POPL (1999)
Anindya Banerjee, Nevin Heintze, Jon G. Riecke
Region Analysis and the Polymorphic Lambda Calculus. LICS (1999)
Anindya Banerjee, David A. Schmidt
Stackability in the Simply-Typed Call-by-Value lambda Calculus. Sci. Comput. Program. 31 (1) (1998)
Anindya Banerjee
A Modular, Polyvariant, and Type-Based Closure Analysis. ICFP (1997)
Anindya Banerjee, David A. Schmidt
Stackability in the Simply-Typed Call-by-Value Lambda Calculus. SAS (1994)
Anindya Banerjee, David A. Schmidt
A Categorical Interpretation of Landin's Correspondence Principle. MFPS (1993)