Conference and Workshop Papers, Technical Reports and 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 IST FET Project 231620 Hats, 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, Thomas Jensen, Gurvan Le Guernic , Ben Livshits , Isabella Mastroeni , Aleksandar Nanevski , David A. Naumann, Aditya Nori, Marco Pistoia , Sriram Rajamani, Venkatesh P. Ranganath, Jon G. Riecke, Stan Rosenberg, David A. Schmidt, Qi Sun

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) , to appear, May 2011. IEEE Computer Society Press. PDF; Last revised, February 2011. The Coq implementation and technical report IMDEA-SW-TR-2010.0
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.
PDF . Last revised, June 2010. To appear.
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. PDF. Last revised, Feb 2010.

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. Last revised, March 2009.

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

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