Anindya Banerjee

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