Papers, Talks and Recent Manuscripts

Research partially supported by National Science Foundation grants EIA-9806835, CCR-0209205, CCR-0296182, ITR-0326577, CNS-0627748; EPSRC grant GR/S03539; IBM T.J. Watson Research Center; Microsoft Research; Madrid Regional Government Project S2009TIC-1465 Prometidos; MICINN Project TIN2009-14599-C03-02 Desafios; EU NoE Project 256980 Nessos.
Co-authors: Martín Abadi, Torben Amtoft, Sruthi Bandhakavi, Mike Barnett, Matthew B. Dwyer, Deepak Garg , Roberto Giacobazzi , John Hatcliff, Nevin Heintze, Neil Immerman , Shachar Itzhaky , Thomas Jensen, Ori Lahav, Gurvan Le Guernic, Ondřej Lhoták , Ben Livshits , Alexander Malkis , Mark Marron , Isabella Mastroeni , Aleksandar Nanevski , David A. Naumann, Aditya Nori, Marco Pistoia , Sriram Rajamani, Venkatesh P. Ranganath, Jon G. Riecke, Stan Rosenberg, Mooly Sagiv , David A. Schmidt, Ilya Sergey, Gordon Stewart, Qi Sun

Language-based Security

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.

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 Mastreoni 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).

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.

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.
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.
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, August 2006.
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.
Note:This paper supercedes the CSFW 2003 and CSFW 2002 papers below.
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.
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)
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.
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. CSFW'03 talk.
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. CSFW'02 talk. Pointerfest talk
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

Verification and Local Reasoning

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. To appear.
PDF; Last revised, April 2015. Coq scripts.

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 containing code and extended version of paper.

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.

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.
PDF; Technical Report; Tool. Last revised, April 2013.

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.

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.

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.

Pointer confinement and data abstraction

Anindya Banerjee and David A. Naumann.
State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings.
PDF; In Aliasing in Object-Oriented Programming, Springer. To appear. Supercedes the ECOOP 2005 paper.

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.

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

Anindya Banerjee and David A. Naumann.
Ownership transfer and abstraction.
PDF; Technical Report, KSU CIS-TR-2004-1. Last revised, October 2003.
Note:This paper supercedes the following FTfJP 2003 paper.

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.

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

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).

Program analysis and Program transformations

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) . To appear, March 2012. Last revised, October 2011.
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.

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 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)
Note:This paper supercedes the following ICFP 1997 paper.

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, 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)

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)
Note:This paper supercedes the following SAS 1994 paper.

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

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)

Miscellaneous papers and thesis

Anindya Banerjee and David A. Naumann.
A Static Analysis for Instance-based Confinement in Java.
PDF; Extended version. Last revised November 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

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.

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)