default search action
Anindya Banerjee 0001
Person information
- affiliation: IMDEA Software Institute, Madrid, Spain
- affiliation (former): Kansas State University, Manhattan, KS, USA
Other persons with the same name
- Anindya Banerjee 0002 — Symantec Research Labs, Pune, India
- Anindya Banerjee 0003 — Wadham College, Oxford, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [i20]Torben Amtoft, Anindya Banerjee:
A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs. CoRR abs/2412.07086 (2024) - 2023
- [j19]Alexander Bagnall, Gordon Stewart, Anindya Banerjee:
Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning. Proc. ACM Program. Lang. 7(PLDI): 1-24 (2023) - [c47]Ramana Nagasamudram, Anindya Banerjee, David A. Naumann:
The WhyRel Prototype for Modular Relational Verification of Pointer Programs. TACAS (2) 2023: 133-151 - [i19]Alexander Bagnall, Gordon Stewart, Anindya Banerjee:
Inductive Reasoning for Coinductive Types. CoRR abs/2301.09802 (2023) - [i18]Ramana Nagasamudram, Anindya Banerjee, David A. Naumann:
The WhyRel Prototype for Relational Verification. CoRR abs/2303.14314 (2023) - [i17]Ramana Nagasamudram, Anindya Banerjee, David A. Naumann:
Alignment complete relational Hoare logics for some and all. CoRR abs/2307.10045 (2023) - 2022
- [j18]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): 25:1-25:136 (2022) - [i16]Alexander Bagnall, Gordon Stewart, Anindya Banerjee:
Formally Verified Samplers From Probabilistic Programs With Loops and Conditioning. CoRR abs/2211.06747 (2022) - [i15]Anindya Banerjee, Ramana Nagasamudram, David A. Naumann:
Making Relational Hoare Logic Alignment Complete. CoRR abs/2212.10338 (2022) - 2021
- [j17]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): 162-167 (2021) - [j16]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): 1-32 (2021) - [c46]Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan:
A formal proof of PAC learnability for decision stumps. CPP 2021: 5-17 - 2020
- [j15]Torben Amtoft, Anindya Banerjee:
A Theory of Slicing for Imperative Probabilistic Programs. ACM Trans. Program. Lang. Syst. 42(2): 6:1-6:71 (2020) - [i14]Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L. Wick, Anindya Banerjee:
Verification of ML Systems via Reparameterization. CoRR abs/2007.06776 (2020) - [i13]Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas:
On Algebraic Abstractions for Concurrent Separation Logics. CoRR abs/2010.12686 (2020)
2010 – 2019
- 2019
- [j14]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): 161:1-161:30 (2019) - [i12]Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, Ignacio Fábregas:
Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. CoRR abs/1904.07136 (2019) - [i11]Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, Mohammad Nikouei:
Data Abstraction and Relational Program Logic. CoRR abs/1910.14560 (2019) - 2018
- [j13]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): 6:1-6:90 (2018) - 2017
- [j12]Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time (Artifact). Dagstuhl Artifacts Ser. 3(2): 04:1-04:4 (2017) - [c45]Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time. ECOOP 2017: 8:1-8:30 - [i10]Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco:
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources. CoRR abs/1709.07741 (2017) - [i9]Torben Amtoft, Anindya Banerjee:
A Theory of Slicing for Probabilistic Control-Flow Graphs. CoRR abs/1711.02246 (2017) - [i8]Torben Amtoft, Anindya Banerjee:
A Semantics for Probabilistic Control-Flow Graphs. CoRR abs/1711.02256 (2017) - 2016
- [c44]Torben Amtoft, Anindya Banerjee:
A Theory of Slicing for Probabilistic Control Flow Graphs. FoSSaCS 2016: 180-196 - [c43]Anindya Banerjee, David A. Naumann, Mohammad Nikouei:
Relational Logic with Framing and Hypotheses. FSTTCS 2016: 11:1-11:16 - [c42]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco:
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. OOPSLA 2016: 92-110 - [i7]Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Concurrent Data Structures Linked in Time. CoRR abs/1604.08080 (2016) - [i6]Anindya Banerjee, David A. Naumann, Mohammad Nikouei:
Relational Logic with Framing and Hypotheses: Technical Report. CoRR abs/1611.08992 (2016) - 2015
- [c41]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. ESOP 2015: 333-358 - [c40]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Mechanized verification of fine-grained concurrent programs. PLDI 2015: 77-87 - [i5]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco:
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects. CoRR abs/1509.06220 (2015) - 2014
- [j11]Alexander Malkis, Anindya Banerjee:
On Automation in the Verification of Software Barriers: Experience Report. J. Autom. Reason. 52(3): 275-329 (2014) - [c39]Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv:
Modular reasoning about heap paths via effectively propositional formulas. POPL 2014: 385-396 - [c38]Anindya Banerjee, David A. Naumann:
A Logical Analysis of Framing for Specifications with Pure Method Calls. VSTTE 2014: 3-20 - [i4]Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee:
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. CoRR abs/1410.0306 (2014) - 2013
- [j10]Anindya Banerjee, David A. Naumann, Stan Rosenberg:
Local Reasoning for Global Invariants, Part I: Region Logic. J. ACM 60(3): 18:1-18:56 (2013) - [j9]Anindya Banerjee, David A. Naumann:
Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. J. ACM 60(3): 19:1-19:73 (2013) - [j8]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): 6:1-6:41 (2013) - [c37]Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, Mooly Sagiv:
Effectively-Propositional Reasoning about Reachability in Linked Data Structures. CAV 2013: 756-772 - [c36]Gordon Stewart, Anindya Banerjee, Aleksandar Nanevski:
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. PPDP 2013: 145-156 - [c35]Anindya Banerjee, David A. Naumann:
A Simple Semantics and Static Analysis for Stack Inspection. Festschrift for Dave Schmidt 2013: 284-308 - [p1]Anindya Banerjee, David A. Naumann:
State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings. Aliasing in Object-Oriented Programming 2013: 319-365 - [e4]Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh, John Hatcliff:
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. EPTCS 129, 2013 [contents] - 2012
- [c34]Mark Marron, Ondrej Lhoták, Anindya Banerjee:
Programming Paradigm Driven Heap Analysis. CC 2012: 41-60 - [c33]Alexander Malkis, Anindya Banerjee:
Verification of software barriers. PPoPP 2012: 313-314 - [c32]Stan Rosenberg, Anindya Banerjee, David A. Naumann:
Decision Procedures for Region Logic. VMCAI 2012: 379-395 - 2011
- [j7]Isabella Mastroeni, Anindya Banerjee:
Modelling declassification policies using abstract domain completeness. Math. Struct. Comput. Sci. 21(6): 1253-1299 (2011) - [c31]Anindya Banerjee:
Modular Verification of Object-Based Programs - Abstract of Invited Talk. FoVeOOS 2011: 1-2 - [c30]Aleksandar Nanevski, Anindya Banerjee, Deepak Garg:
Verification of Information Flow and Access Control Policies with Dependent Types. IEEE Symposium on Security and Privacy 2011: 165-179 - 2010
- [c29]David A. Naumann, Anindya Banerjee:
Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. ESOP 2010: 2-22 - [c28]Stan Rosenberg, Anindya Banerjee, David A. Naumann:
Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. VSTTE 2010: 183-198 - [e3]Anindya Banerjee, Deepak Garg:
Proceedings of the 2010 Workshop on Programming Languages and Analysis for Security, PLAS 2010, Toronto, ON, Canada, 10 June, 2010. ACM 2010, ISBN 978-1-60558-827-8 [contents]
2000 – 2009
- 2009
- [c27]Anindya Banerjee:
Semantics and Enforcement of Expressive Information Flow Policies. Formal Aspects in Security and Trust 2009: 1-3 - [c26]V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, Anindya Banerjee:
Merlin: specification inference for explicit information flow problems. PLDI 2009: 75-86 - [c25]Avraham Shinnar, Marco Pistoia, Anindya Banerjee:
A language for information flow: dynamic tracking in multiple interdependent dimensions. PLAS 2009: 125-131 - [e2]Anindya Banerjee:
Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs, FTfJP 2009, Genova, Italy, July 6, 2009. ACM 2009, ISBN 978-1-60558-540-6 [contents] - 2008
- [c24]Anindya Banerjee, David A. Naumann, Stan Rosenberg:
Regional Logic for Local Reasoning about Global Invariants. ECOOP 2008: 387-411 - [c23]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: 70-76 - [c22]Anindya Banerjee, David A. Naumann, Stan Rosenberg:
Expressive Declassification Policies and Modular Static Enforcement. SP 2008: 339-353 - [c21]Anindya Banerjee, Michael Barnett, David A. Naumann:
Boogie Meets Regions: A Verification Experience Report. VSTTE 2008: 177-191 - 2007
- [j6]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): 3-28 (2007) - [j5]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): 27 (2007) - [c20]Torben Amtoft, Anindya Banerjee:
Verification condition generation for conditional information flow. FMSE 2007: 2-11 - [c19]Anindya Banerjee, David A. Naumann, Stan Rosenberg:
Towards a logical account of declassification. PLAS 2007: 61-66 - [c18]Marco Pistoia, Anindya Banerjee, David A. Naumann:
Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. S&P 2007: 149-163 - [c17]Anindya Banerjee, Roberto Giacobazzi, Isabella Mastroeni:
What You Lose is What You Leak: Information Leakage in Declassification Policies. MFPS 2007: 47-66 - 2006
- [c16]Gurvan Le Guernic, Anindya Banerjee, Thomas P. Jensen, David A. Schmidt:
Automata-Based Confidentiality Monitoring. ASIAN 2006: 75-89 - [c15]Torben Amtoft, Sruthi Bandhakavi, Anindya Banerjee:
A logic for information flow in object-oriented programs. POPL 2006: 91-102 - 2005
- [j4]Anindya Banerjee, David A. Naumann:
Ownership confinement ensures representation independence for object-oriented programs. J. ACM 52(6): 894-960 (2005) - [j3]Anindya Banerjee, David A. Naumann:
Stack-based access control and secure information flow. J. Funct. Program. 15(2): 131-177 (2005) - [c14]Anindya Banerjee, David A. Naumann:
State Based Ownership, Reentrance, and Encapsulation. ECOOP 2005: 387-411 - [c13]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: 77-93 - [e1]Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld:
Language-Based Security, 5.-10. October 2003. Dagstuhl Seminar Proceedings 03411, IBFI, Schloss Dagstuhl, Germany 2005 [contents] - 2004
- [c12]Anindya Banerjee, David A. Naumann:
History-Based Access Control and Secure Information Flow. CASSIS 2004: 27-48 - [c11]Qi Sun, Anindya Banerjee, David A. Naumann:
Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. SAS 2004: 84-99 - [c10]Torben Amtoft, Anindya Banerjee:
Information Flow Analysis in Logical Form. SAS 2004: 100-115 - 2003
- [j2]Anindya Banerjee, Thomas P. Jensen:
Modular Control-Flow Analysis with Rank 2 Intersection Types. Math. Struct. Comput. Sci. 13(1): 87-124 (2003) - [c9]Anindya Banerjee, David A. Naumann:
Using Access Control for Secure Information Flow in a Java-like Language. CSFW 2003: 155-169 - [i3]Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld:
03411 Final Report - Language Based Security. Language Based Security 2003 - [i2]Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld:
03411 Abstracts Collection - Language Based Security. Language Based Security 2003 - 2002
- [c8]Anindya Banerjee, David A. Naumann:
Secure Information Flow and Pointer Confinement in a Java-like Language. CSFW 2002: 253- - [c7]Anindya Banerjee, David A. Naumann:
Representation independence, confinement and access control [extended abstract]. POPL 2002: 166-177 - [i1]Anindya Banerjee, David A. Naumann:
Ownership Confinement Ensures Representation Independence for Object-Oriented Programs. CoRR cs.PL/0212003 (2002) - 2001
- [c6]Anindya Banerjee, Nevin Heintze, Jon G. Riecke:
Design and Correctness of Program Transformations Based on Control-Flow Analysis. TACS 2001: 420-447
1990 – 1999
- 1999
- [c5]Anindya Banerjee, Nevin Heintze, Jon G. Riecke:
Region Analysis and the Polymorphic Lambda Calculus. LICS 1999: 88-97 - [c4]Martín Abadi, Anindya Banerjee, Nevin Heintze, Jon G. Riecke:
A Core Calculus of Dependency. POPL 1999: 147-160 - 1998
- [j1]Anindya Banerjee, David A. Schmidt:
Stackability in the Simply-Typed Call-by-Value lambda Calculus. Sci. Comput. Program. 31(1): 47-73 (1998) - 1997
- [c3]Anindya Banerjee:
A Modular, Polyvariant, and Type-Based Closure Analysis. ICFP 1997: 1-10 - 1994
- [c2]Anindya Banerjee, David A. Schmidt:
Stackability in the Simply-Typed Call-by-Value Lambda Calculus. SAS 1994: 131-146 - 1993
- [c1]Anindya Banerjee, David A. Schmidt:
A Categorical Interpretation of Landin's Correspondence Principle. MFPS 1993: 587-602
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-21 00:07 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint