Papers and Talks

2023

• Alexander Bagnall, Gordon Stewart and Anindya Banerjee.
  Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning.
  In Proceedings of the ACM on Programming Languages, 7(PLDI), Article no. 106, pp. 1--24, June 2023.
  [PDF (local copy) | @ACM | arXiv]
• Ramana Nagasamudram, Anindya Banerjee and David A. Naumann.
  The WhyRel Prototype for Modular Relational Verification of Pointer Programs.
  In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS (2)), pp.133--151, April 2023.
  [PDF | arXiv]

2022

• Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, and Mohammad Nikouei.
  A Relational Program Logic with Data Abstraction and Dynamic Framing.
  In ACM Transactions on Programming Languages and Systems (TOPLAS)), 44(4), 25:1--25:136, December 2022.
  [PDF (local copy, with index) | @ACM]

2021

• František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas.
  On Algebraic Abstractions for Concurrent Separation Logics.
  In Proceedings of the ACM on Programming Languages, 5(POPL), pp. 1--32, January 2021.
  [PDF (local copy) | @ACM | arXiv]
• Joseph Tassarotti, Koundiniya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan.
  A Formal Proof of PAC Learnability for Decision Stumps.
  In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), January 2021.
  [PDF (local copy)]

2020

• Torben Amtoft and Anindya Banerjee.
  A Theory of Slicing for Imperative Probabilistic Programs.
  In ACM Transactions on Programming Languages and Systems (TOPLAS) 42(2), 6:1--6:71, April 2020.
  [PDF (local copy) | @ACM]
  Supercedes the FoSSaCS 2016 paper.

2019

• Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas.
  Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations.
  In Proceedings of the ACM on Programming Languages, 3(OOPSLA), pp. 161:1--161:30, October 2019.
  [PDF (local copy) | @ACM | arXiv]

2018

• Anindya Banerjee, David A. Naumann, and Mohammad Nikouei.
  A Logical Analysis of Framing for Specifications with Pure Method Calls.
  In ACM Transactions on Programming Languages and Systems (TOPLAS) 40(2), article 6, June 2018.
  [PDF (local copy, with index) | @ACM]
  Supercedes the VSTTE 2014 paper.

2017

• Torben Amtoft and Anindya Banerjee.
  A Semantics for Probabilistic Control-Flow Graphs.
  Last revised November 2017.
  [arXiv]
• Torben Amtoft and Anindya Banerjee.
  A Theory of Slicing for Probabilistic Control-Flow Graphs.
  Last revised November 2017. Supercedes the FoSSaCS 2016 paper.
  [arXiv]
• Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee
  Concurrent Data Structures Linked in Time.
  In Proceedings of the Thirty-first European Conference on Object-oriented Programming (ECOOP), June 2017
  [arXiv]

2016

• Anindya Banerjee, David A. Naumann, and Mohammad Nikouei.
  Relational Logic with Framing and Hypotheses.
  In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) , December 2016.
  [PDF; Last revised October 2016 | arXiv]
• Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco.
  Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects.
  In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) , November 2016.
  [PDF | Project page]
• Torben Amtoft and Anindya Banerjee.
  A Theory of Slicing for Probabilistic Control-Flow Graphs.
  In Nineteenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) , April 2016.
  [PDF; Last revised January 2016 | Technical Report]

2015

• Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee.
  Mechanized Verification of Fine-grained Concurrent Programs.
  In Thirtysixth ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI) , June 2015.
  [PDF | Coq sources | Project page]
• Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee.
  Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.
  In Twentyfourth European Symposium on Programming (ESOP) , April 2015.
  [PDF | Project page]

2014

• Anindya Banerjee and David A. Naumann.
  A Logical Analysis of Framing for Specifications with Pure Method Calls.
  In Verified Software: Theories, Tools and Experiments - 6th International Conference (VSTTE) July, 2014.
  PDF; Last revised, July 2014.

• Alexander Malkis and Anindya Banerjee.
  On Automation in the Verification of Software Barriers: Experience Report.
  Journal of Automated Reasoning (JAR) 52(3), pp. 275--329, March 2014.
  PDF; The experiments.
• Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski and Mooly Sagiv.
  Modular Reasoning about Heap Paths via Effectively Propositional Formulas.
  In Proceedings of the Forty-first Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 385-396, January 2014.
  PDF; Last revised, November 2013.

2013

• Anindya Banerjee and David A. Naumann.
  A Simple Semantics and Static Analysis for Stack Inspection.
  In Semantics, Abstract Interpretation and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday. Electronic Proceedings in Theoretical Computer Science (EPTCS) 129. PDF
• Gordon Stewart, Anindya Banerjee and Aleksandar Nanevski.
  Dependent Types for Enforcement of Information Flow and Erasure Policies in Heterogeneous Data Structures.
  In 15th International Conference on Principles and Practice of Declarative Programming (PPDP), pp. 145--156, September 2013.
  PDF; Coq implementation; Last revised, June 2013.

• Aleksandar Nanevski, Anindya Banerjee and Deepak Garg.
  Dependent Type Theory for Verification of Information Flow and Access Control Policies.
  ACM Transactions on Programming Languages and Systems (TOPLAS) 35(2), article 6, July 2013. PDF
  Supercedes the S& P 2011 paper.
  
• Anindya Banerjee and David A. Naumann.
  Local Reasoning for Global Invariants, Part II: Dynamic Boundaries
  Journal of the ACM (JACM) 60(3), article 19, June 2013. PDF
• Anindya Banerjee, David A. Naumann and Stan Rosenberg.
  Local Reasoning for Global Invariants, Part I: Region Logic
  Journal of the ACM (JACM) 60(3), article 18, June 2013. PDF
• Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski and Mooly Sagiv.
  Effectively-Propositional Reasoning about Reachability in Linked Data Structures.
  In 25th International Conference on Computer Aided Verification (CAV), July 2013.
  Lecture Notes in Computer Science, Vol. 8044, pp. 756--772. Springer. PDF; Technical Report; Tool. Last revised, April 2013.
• Anindya Banerjee and David A. Naumann.
  State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings.
  In Dave Clarke, James Noble, and Tobias Wrigstad, editors, Aliasing in Object-Oriented Programming.
  Lecture Notes in Computer Science, Vol. 7850, pp. 319--365. Springer. PDF

2012

• Mark Marron, Ondrej Lhoták and Anindya Banerjee.
  Program Paradigm Driven Heap Analysis
  In Proceedings of the Twenty-first International Conference on Compiler Construction (CC) . Last revised, October 2011.

• Stan Rosenberg, Anindya Banerjee and David A. Naumann.
  Decision Procedures for Region Logic.
  In Proceedings of the Thirteenth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) , January 2012.
  Lecture Notes in Computer Science, Vol. 7148, pp. 379--395. Springer. PDF; Last revised, November 2011.

2011

• Aleksandar Nanevski, Anindya Banerjee and Deepak Garg.
  Verification of Information Flow and Access Control Policies with Dependent Types.
  In Proceedings of the 2011 IEEE Symposium on Security and Privacy (S& P) , pp. 165--179, May 2011. IEEE Computer Society Press. PDF; Last revised, February 2011. The Coq implementation and technical report IMDEA-SW-TR-2010.0. Superceded by the TOPLAS 2013 paper.
• Benjamin Livshits, Aditya Nori, Sriram Rajamani and Anindya Banerjee
  Merlin: Specification Inference for Explicit Information Flow Problems. In Mining Software Specifications: Methodologies and Applications , Chapman & Hall/CRC Data Mining and Knowledge Discovery Series, ISBN: 9781439806265. April 2011.
• Isabella Mastroeni and Anindya Banerjee.
  Modelling Declassification Policies using Abstract Domain Completeness.
  In Mathematical Structures in Computer Science, vol.21, pp.1253-1299, 2011. (© Cambridge University Press).

2010

• Stan Rosenberg, Anindya Banerjee and David A. Naumann
  Local Reasoning and Dynamic Framing for the Composite Pattern and its Clients.
  In Third International Conference on Verified Software: Theories,Tools, and Experiments (VSTTE'10), August 2010.
  Lecture Notes in Computer Science, Vol. 6217, pp. 183--198. Springer. PDF. Last revised, June 2010.

• David A. Naumann and Anindya Banerjee
  Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions (with appendix).
  In Nineteenth European Symposium on Programming (ESOP) , March 2010. Lecture Notes in Computer Science, Vol. 6012, pp. 2--22. Springer. PDF. Last revised, Feb 2010.

2009

• Benjamin Livshits, Aditya Nori, Sriram Rajamani and Anindya Banerjee
  Merlin: Specification Inference for Explicit Information Flow Problems.
  In 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) , pp. 75--86, June 2009. PDF; ACM Press.
• Avraham Shinnar, Marco Pistoia and Anindya Banerjee.
  A Language for Information Flow: Dynamic Tracking in Multiple Interdependent Dimensions.
  In Proceedings of 2009 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS) , pp. 125--131, June 2009. PDF; ACM Press. Last revised, May 2009; Research Report, RC 2451 IBM TJ Watson Research Center. Last revised, April 2008.

2008

• Anindya Banerjee, Mike Barnett and David A. Naumann.
  Boogie Meets Regions: a Verification Experience Report.
  In Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'08), Lecture Notes in Computer Science, Vol. 5295, pp. 177--191, October 2008. Springer. PDF; Technical Report MSR-TR-2008-79; Last revised, May 2008.
  Download Boogie PL code for examples in paper.

• Anindya Banerjee, David A. Naumann and Stan Rosenberg.
  Regional Logic for Local Reasoning about Global Invariants.
  In Proceedings of the Twenty-second European Conference on Object-oriented Programming (ECOOP) , pp. 387-411, volume 5142 of Lecture Notes in Computer Science, Springer-Verlag, July 2008. PDF; Last revised, May 2008.

• Anindya Banerjee, David A. Naumann and Stan Rosenberg.
  Expressive Declassification Policies and their Modular Static Enforcement.
  In Proceedings of the 2008 IEEE Symposium on Security and Privacy (S& P) , pp. 339--353, May 2008. IEEE Computer Society Press. PDF; Last revised, March 2008.

2007

• Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer and John Hatcliff.
  A New Foundation for Control-Dependence and Slicing for Modern Program Structures.
  ACM Transactions on Programming Languages and Systems (TOPLAS) 29(5), August 2007.

• Torben Amtoft and Anindya Banerjee.
  Verification Condition Generation for Conditional Information Flow.
  In Fifth ACM Workshop on Formal Methods in Security Engineering (FMSE) , pp. 2--11, November 2007. ACM Press. PDF; Last revised, June 2007. KSU CIS TR-2007-2; Last revised, June 2007.

• Anindya Banerjee, David A. Naumann and Stan Rosenberg.
  Towards a Logical Account of Declassification (Short Paper).
  In Proceedings of the 2007 ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS) , pp. 61--65, June 2007. ACM Press. PDF; Last revised, May 2007.

• Marco Pistoia, Anindya Banerjee and David A. Naumann
  Beyond stack inspection: A unified access-control and information-flow security model.
  In Proceedings of the 2007 IEEE Symposium on Security and Privacy (S& P), pp. 149--163, May 2007.
  IEEE Computer Society Press. PDF. Last revised, March 2007.

• Anindya Banerjee, Roberto Giacobazzi and Isabella Mastroeni.
  What you lose is what you leak: Information leakage in declassification policies.
  In Proceedings of the Twenty-Third Conference on Mathematical Foundations of Programming Semantics (MFPS), pp. 47-66, volume 173 of Electronic Notes in Theoretical Computer Science, Elsevier, B.V., April 2007. PDF; Last revised, February 2007.

• Torben Amtoft and Anindya Banerjee.
  A Logic for Information Flow Analysis with an Application to Forward Slicing of Simple Imperative Programs.
  PDF; Science of Computer Programming 64(1), pp. 3-28, January 2007.
  Supercedes the SAS 2004 paper Information Flow Analysis in Logical Form.

2006

• Gurvan Le Guernic, Anindya Banerjee, Thomas Jensen and David A. Schmidt.
  Automata-based Confidentiality Monitoring.
  In Proceedings of the Eleventh Annual Asian Computing Science Conference (ASIAN). Lecture Notes in Computer Science, Vol. 4435, pp. 75--89, December 2006. Springer.

• Anindya Banerjee and David A. Naumann.
  A Logical Account of Secure Declassification. PDF; Last revised, April 2006.
  Superceded by PLAS 2007 and S& P 2008 papers.

• Torben Amtoft, Sruthi Bandhakavi and Anindya Banerjee.
  A Logic for Information Flow in Object-Oriented Programs.
  In Proceedings of the Thirty-third Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 91-102, January 2006. Talk at POPL; PDF; Last revised, November 2005; Technical Report, KSU CIS-TR-2005-1; Last revised, September 2005.

2005

• Anindya Banerjee and David A. Naumann.
  Ownership Confinement Ensures Representation Independence in Object-Oriented Programs.
  Journal of the ACM (JACM) 52(6), pp. 894-960, November 2005.
  PDF; Technical Report KSU CIS-TR-2004-6 and SIT CS-TR-2004-14.
  This supercedes the POPL 2002 version, Representation Independence, Confinement, and Access Control , improving and extending it to include a static analysis and substantial examples.

• Anindya Banerjee and David A. Naumann.
  Stack-based Access Control and Secure Information Flow.
  Journal of Functional Programming 15(2), pp. 131-177, Special issue on Language-based Security, March 2005.
  PDF; Dagstuhl Seminar 03411 talk.
  This paper supercedes the CSFW 2003 and CSFW 2002 papers below.

• Anindya Banerjee and David A. Naumann.
  State based ownership, reentrance, and encapsulation.
  In Proceedings of the Nineteenth European Conference on Object-oriented Programming (ECOOP) , pp. 387-411, volume 3586 of Lecture Notes in Computer Science, Springer-Verlag, July 2005.
  PDF; Last revised, May 2005.

• Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, Matthew B. Dwyer and John Hatcliff.
  A New Foundation for Control-Dependence and Slicing for Modern Program Structures.
  In Proceedings of the European Symposium of Programming (ESOP) , April 2005. Lecture Notes in Computer Science, Vol. 3444, pp. 77--93.
  PDF (© Springer-Verlag); Technical Report, TR-2004-8, SAnToS Laboratory. Last revised, October 2004.

• Anindya Banerjee and David A. Naumann.
  History-based Access Control and Secure Information Flow.
  In Proceedings of the workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Cards (CASSIS), pp. 27-48, volume 3362 of Lecture Notes in Computer Science, Springer-Verlag, March 2005.
  PDF (© Springer-Verlag)

2004

• Anindya Banerjee and David A. Naumann.
  State based ownership and generics.
  PDF; Technical Report, CS-2004-11, Stevens Institute of Technolgy and KSU CIS-TR-2004-5. Last revised, December 2004.

• Torben Amtoft and Anindya Banerjee
  Information flow analysis in logical form.
  In Proceedings of the Eleventh International Static Analysis Symposium (SAS) , pp. 100-115, volume 3148 of Lecture Notes in Computer Science, Springer-Verlag, August 2004. PDF (© Springer-Verlag)
  Technical Report KSU CIS-TR-2004-3. Last revised, May 2004.

• Qi Sun, Anindya Banerjee and David A. Naumann
  Modular and constraint-based information flow inference for an object-oriented language.
  In Proceedings of the Eleventh International Static Analysis Symposium (SAS) , pp. 84-99, volume 3148 of Lecture Notes in Computer Science, Springer-Verlag, August 2004. PDF (© Springer-Verlag). Last revised, May 2004.

2003

• Anindya Banerjee and David A. Naumann.
  Ownership transfer and abstraction.
  PDF; Technical Report, KSU CIS-TR-2004-1. Last revised, October 2003.
  

• Anindya Banerjee and David A. Naumann.
  Ownership: transfer, sharing, and encapsulation.
  In ECOOP Workshop on Formal Techniques for Java-like Programs (FTfJP) , July 2003.
  PDF. Last revised May 2003.

• Anindya Banerjee and David A. Naumann.
  Using Access Control for Secure Information Flow in a Java-like Language.
  In Proceedings of the Sixteenth IEEE Computer Security Foundations Workshop (CSFW) , pp. 155-169, June 2003.
  IEEE Computer Society Press. PDF. Last revised April 2003. CSFW'03 talk.

• Anindya Banerjee and Thomas Jensen.
  Modular Control-flow Analysis with Rank 2 Intersection Types.
  Mathematical Structures in Computer Science 13(1), pp. 87-124, February 2003.
  Cambridge University Press. PDF (Preprint)

2002

• Anindya Banerjee and David A. Naumann.
  Secure Information Flow and Pointer Confinement in a Java-like Language.
  In Proceedings of the Fifteenth IEEE Computer Security Foundations Workshop (CSFW) , pp. 253-267, June 2002.
  IEEE Computer Society Press. PDF. Last revised April 2002. CSFW'02 talk. Pointerfest talk

• Anindya Banerjee and David A. Naumann.
  Representation independence, Confinement, and Access Control.
  In Proceedings of the Twenty-ninth Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 166-177, January 2002. ACM Press. PDF (Extended Abstract with appendices). Last revised November 2001.
  

2001

• Anindya Banerjee and David A. Naumann.
  A Static Analysis for Instance-based Confinement in Java.
  PDF; Extended version. Last revised November 2001.

• Anindya Banerjee, Nevin Heintze and Jon G. Riecke.
  Design and Correctness of Program Transformations based on Control-flow Analysis.
  Invited paper, Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS), pp. 420-447, volume 2215 of Lecture Notes in Computer Science, Springer-Verlag, October 2001. PS (© Springer-Verlag). Last revised September 2001.

• Anindya Banerjee and David A. Naumann.
  A Simple Semantics and Static Analysis for Java Security.
  Technical Report 2001-1, Stevens Institute of Technology, July 2001. PDF

2000

1999

• Anindya Banerjee, Nevin Heintze and Jon G. Riecke.
  Region Analysis and the Polymorphic Lambda Calculus.
  In Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS) , pp. 88-97, July 1999.
  IEEE Computer Society Press. PS (Extended abstract)

• Martín Abadi, Anindya Banerjee, Nevin Heintze and Jon G. Riecke.
  A Core Calculus of Dependency.
  In Proceedings of the Twenty-sixth Annual ACM Symposium on Principles of Programming Languages (POPL), pp. 147-160, January 1999. ACM Press. PS

1998

• Anindya Banerjee and David A. Schmidt.
  Stackability in the Simply-Typed Call-by-Value Lambda Calculus.
  Science of Computer Programming, Volume 31, pp. 47-73, 1998. PS (Preprint)

1997

• Anindya Banerjee.
  A Modular, Polyvariant and Type-based Closure Analysis.
  In Proceedings of the Second ACM International Conference on Functional Programming (ICFP), pp. 1-10, June 1997. ACM Press. PS

1996

1995

• Anindya Banerjee.
  The Semantics and Implementation of Bindings in Higher-Order Programming Languages.
  Ph.D. thesis, Department of Computing and Information Sciences, Kansas State University,1995.

1994

• Anindya Banerjee and David A. Schmidt.
  Stackability in the Simply-Typed Call-by-Value Lambda Calculus.
  In Proceedings of the First International Static Analysis Symposium (SAS), pp. 136-151, volume 864 of Lecture Notes in Computer Science, Springer-Verlag, September 1994. PS (© Springer-Verlag)

• Anindya Banerjee and David A. Schmidt.
  A Categorical Interpretation of Landin's Correspondence Principle.
  In Proceedings of the Ninth Conference on Mathematical Foundations of Programming Semantics (MFPS), pp. 587-602, volume 802 of Lecture Notes in Computer Science, Springer-Verlag, 1994. PS (© Springer-Verlag)