[1] Alexander Bagnall, Gordon Stewart, and Anindya Banerjee. Formally verified samplers from probabilistic programs with loops and conditioning. Proc. ACM Program. Lang., 7(PLDI):1--24, 2023. [ bib | DOI | http ]
[2] Ramana Nagasamudram, Anindya Banerjee, and David A. Naumann. The whyrel prototype for modular relational verification of pointer programs. In TACAS 2023, Part II, number 13994 in Lecture Notes in Computer Science, pages 1--19. Springer Nature, 2023. [ bib | DOI | http ]
[3] Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, and Mohammad Nikouei. A relational program logic with data abstraction and dynamic framing. ACM Trans. Program. Lang. Syst., 44(4):1--136, 2022. [ bib | DOI | http ]
[4] Anindya Banerjee, Sankar Basu, Erik Brunvand, Pinaki Mazumder, Rance Cleaveland, Gurdip Singh, Margaret Martonosi, and Fernanda Pembleton. Navigating the seismic shift of post-moore computer systems design. IEEE Micro, 41(6):162--167, 2021. [ bib | DOI | http ]
[5] Frantisek Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas. On algebraic abstractions for concurrent separation logics. Proc. ACM Program. Lang., 5(POPL):1--32, 2021. [ bib | DOI | http ]
[6] Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan. A formal proof of PAC learnability for decision stumps. In CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 5--17. ACM, 2021. [ bib | DOI | http ]
[7] Torben Amtoft and Anindya Banerjee. A theory of slicing for imperative probabilistic programs. ACM Trans. Program. Lang. Syst., 42(2):6:1--6:71, 2020. [ bib | DOI | http ]
[8] Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas. Specifying concurrent programs in separation logic: Morphisms and simulations. PACMPL, 3(OOPSLA):161:1--161:30, 2019. [ bib ]
[9] Anindya Banerjee, David A. Naumann, and Mohammad Nikoueki. A logical analysis of framing for specifications with pure method calls. ACM Trans. Program. Lang. Syst., 40(2):6:1--6:90, 2018. [ bib ]
[10] Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Concurrent data structures linked in time. In ECOOP, pages 8:1--8:30, 2017. [ bib ]
[11] Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. Relational logic with framing and hypotheses. In FSTTCS, pages 11:1--11:16, 2016. [ bib ]
[12] Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. In OOPSLA, pages 92--110, 2016. [ bib ]
[13] Torben Amtoft and Anindya Banerjee. A theory of slicing for probabilistic control flow graphs. In FoSSaCS, Lecture Notes in Computer Science, pages 180--196, 2016. [ bib ]
[14] Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized verification of fine-grained concurrent programs. In PLDI, pages 77--87, 2015. [ bib ]
[15] Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Specifying and verifying concurrent algorithms with histories and subjectivity. In ESOP, volume 9032 of Lecture Notes in Computer Science, pages 333--358, 2015. [ bib ]
[16] 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 2014, Vienna, Austria, July 17-18, 2014, Revised Selected Papers, pages 3--20, 2014. [ bib ]
[17] Alexander Malkis and Anindya Banerjee. On automation in the verification of software barriers: Experience report. Journal of Automated Reasoning, 52(3):275--329, 2014. [ bib ]
[18] Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, and Mooly Sagiv. Modular reasoning about heap paths via effectively propositional formulas. In POPL, pages 385--396, 2014. Last revised, April 2013. [ bib ]
[19] Anindya Banerjee and David A. Naumann. A simple semantics and static analysis for stack inspection. In Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh, and John Hatcliff, editors, Proceedings 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, volume 129 of Electronic Proceedings in Theoretical Computer Science, pages 284--308. Open Publishing Association, 2013. [ bib | DOI ]
[20] Gordon Stewart, Anindya Banerjee, and Aleksandar Nanevski. Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures. In PPDP, pages 145--156, 2013. Last revised, June 2013. [ bib ]
[21] Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Local reasoning for global invariants, part i: Region logic. Journal of the ACM, 60(3):18, 2013. [ bib ]
[22] Anindya Banerjee and David A. Naumann. Local reasoning for global invariants, part ii: Dynamic boundaries. Journal of the ACM, 60(3):19, 2013. [ bib ]
[23] Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. Dependent type theory for verification of information flow and access control policies. ACM Trans. Program. Lang. Syst., 35(2):6, 2013. [ bib ]
[24] Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, and Mooly Sagiv. Effectively-propositional reasoning about reachability in linked data structures. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 756--772. Springer, 2013. Last revised, April 2013. [ bib ]
[25] 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, volume 7850 of Lecture Notes in Computer Science, pages 319--365. Springer, 2013. [ bib ]
[26] Mark Marron, Ondrej Lhoták, and Anindya Banerjee. Program paradigm driven heap analysis. In CC, volume 7210 of Lecture Notes in Computer Science, pages 41--60. Springer, 2012. Last revised, October 2011. [ bib ]
[27] Stan Rosenberg, Anindya Banerjee, and David A. Naumann. Decision procedures for region logic. In VMCAI, volume 7148 of Lecture Notes in Computer Science, pages 379--395. Springer, 2012. Last revised, November 2011. [ bib ]
[28] Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. Verification of information flow and access control policies with dependent types. In IEEE Symposium on Security and Privacy, pages 165--179, 2011. [ bib ]
[29] V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, and Anindya Banerjee. Merlin: specification inference for explicit information flow problems. In David Lo, Siau-Cheng Khoo, Jiawei Han, and Chao Liu, editors, Mining Software Specifications, chapter 11, pages 377--410. Chapman & Hall/CRC, 2011. [ bib ]
[30] Isabella Mastroeni and Anindya Banerjee. Modelling declassification policies using abstract domain completeness. Mathematical Structures in Computer Science, 21:1253--1299, 2011. [ bib ]
[31] David A. Naumann and Anindya Banerjee. Dynamic boundaries: Information hiding by second order framing with first order assertions. In ESOP, pages 2--22, 2010. [ bib ]
[32] Stan Rosenberg, Anindya Banerjee, and David A. Naumann. Local reasoning and dynamic framing for the composite pattern and its clients. In VSTTE, pages 183--198, 2010. [ bib ]
[33] Anindya Banerjee. Semantics and enforcement of expressive information flow policies. In Formal Aspects in Security and Trust, pages 1--3, 2009. [ bib ]
[34] Avraham Shinnar, Marco Pistoia, and Anindya Banerjee. A language for information flow: dynamic tracking in multiple interdependent dimensions. In PLAS, pages 125--131, 2009. [ bib ]
[35] V. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, and Anindya Banerjee. Merlin: specification inference for explicit information flow problems. In PLDI, pages 75--86, 2009. [ bib ]
[36] Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Regional logic for local reasoning about global invariants. In ECOOP, pages 387--411, 2008. [ bib ]
[37] Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary T. Leavens, Peter Müller, and Tobias Wrigstad. Formal techniques for java-like programs. In ECOOP Workshops, pages 70--76, 2008. [ bib ]
[38] Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Expressive declassification policies and modular static enforcement. In IEEE Symposium on Security and Privacy, pages 339--353, 2008. [ bib ]
[39] Anindya Banerjee, Michael Barnett, and David A. Naumann. Boogie meets regions: A verification experience report. In VSTTE, pages 177--191, 2008. [ bib ]
[40] Torben Amtoft and Anindya Banerjee. Verification condition generation for conditional information flow. In FMSE, pages 2--11, 2007. [ bib ]
[41] Marco Pistoia, Anindya Banerjee, and David A. Naumann. Beyond stack inspection: A unified access-control and information-flow security model. In IEEE Symposium on Security and Privacy, pages 149--163, 2007. [ bib ]
[42] Anindya Banerjee, David A. Naumann, and Stan Rosenberg. Towards a logical account of declassification. In PLAS, pages 61--66, 2007. [ bib ]
[43] Venkatesh Prasad Ranganath, Torben Amtoft, Anindya Banerjee, John Hatcliff, and Matthew B. Dwyer. A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst., 29(5), 2007. [ bib ]
[44] Anindya Banerjee, Roberto Giacobazzi, and Isabella Mastroeni. What you lose is what you leak: Information leakage in declassification policies. Electr. Notes Theor. Comput. Sci., 173:47--66, 2007. [ bib ]
[45] Torben Amtoft and 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. [ bib ]
[46] Gurvan Le Guernic, Anindya Banerjee, Thomas P. Jensen, and David A. Schmidt. Automata-based confidentiality monitoring. In ASIAN, pages 75--89, 2006. [ bib ]
[47] Torben Amtoft, Sruthi Bandhakavi, and Anindya Banerjee. A logic for information flow in object-oriented programs. In POPL, pages 91--102, 2006. [ bib ]
[48] Anindya Banerjee, Heiko Mantel, David A. Naumann, and Andrei Sabelfeld, editors. Language-Based Security, 5.-10. October 2003, volume 03411 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany IBFI, Schloss Dagstuhl, Germany, 2005. [ bib ]
[49] Anindya Banerjee and David A. Naumann. State based ownership, reentrance, and encapsulation. In ECOOP, pages 387--411, 2005. [ bib ]
[50] 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 ESOP, pages 77--93, 2005. [ bib ]
[51] Anindya Banerjee and David A. Naumann. Ownership confinement ensures representation independence for object-oriented programs. J. ACM, 52(6):894--960, 2005. [ bib ]
[52] Anindya Banerjee and David A. Naumann. Stack-based access control and secure information flow. J. Funct. Program., 15(2):131--177, 2005. [ bib ]
[53] Anindya Banerjee and David A. Naumann. History-based access control and secure information flow. In CASSIS, pages 27--48, 2004. [ bib ]
[54] Torben Amtoft and Anindya Banerjee. Information flow analysis in logical form. In SAS, pages 100--115, 2004. [ bib ]
[55] Qi Sun, Anindya Banerjee, and David A. Naumann. Modular and constraint-based information flow inference for an object-oriented language. In SAS, pages 84--99, 2004. [ bib ]
[56] Anindya Banerjee and David A. Naumann. Using access control for secure information flow in a java-like language. In CSFW, pages 155--169, 2003. [ bib ]
[57] Anindya Banerjee and Thomas P. Jensen. Modular control-flow analysis with rank 2 intersection types. Mathematical Structures in Computer Science, 13(1):87--124, 2003. [ bib ]
[58] Anindya Banerjee and David A. Naumann. Secure information flow and pointer confinement in a java-like language. In CSFW, pages 253--, 2002. [ bib ]
[59] Anindya Banerjee and David A. Naumann. Representation independence, confinement and access control [extended abstract]. In POPL, pages 166--177, 2002. [ bib ]
[60] Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Design and correctness of program transformations based on control-flow analysis. In TACS, pages 420--447, 2001. [ bib ]
[61] Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. Region analysis and the polymorphic lambda calculus. In LICS, pages 88--97, 1999. [ bib ]
[62] Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In POPL, pages 147--160, 1999. [ bib ]
[63] Anindya Banerjee and David A. Schmidt. Stackability in the simply-typed call-by-value lambda calculus. Sci. Comput. Program., 31(1):47--73, 1998. [ bib ]
[64] Anindya Banerjee. A modular, polyvariant, and type-based closure analysis. In ICFP, pages 1--10, 1997. [ bib ]
[65] Anindya Banerjee and David A. Schmidt. Stackability in the simply-typed call-by-value lambda calculus. In SAS, pages 131--146, 1994. [ bib ]
[66] Anindya Banerjee and David A. Schmidt. A categorical interpretation of landin's correspondence principle. In MFPS, pages 587--602, 1993. [ bib ]

This file was generated by bibtex2html 1.99.