flowspecs
Publications

Spartan Jester: End-to-end Information Flow Control for Hybrid Android Applications, Julian Sexton, Andrey Chudnov, David A. Naumann. in IEEE Mobile Security Technologies, 2017.

Hypercollecting Semantics and its Application to Static Analysis of Information Flow, Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, and Frederic Tronel. In ACM Symposium on Principles of Programming Languages, 2017.

Relational Logic with Framing and Hypotheses, Anindya Banerjee, David A. Naumann, Mohammad Nikouei. In 36th Conference on Foundations of Software Technology and Theoretical Computer Science , 2016.

Calculational Design of Information Flow Monitors, Mounir Assaf and David A. Naumann. In IEEE Computer Security Foundations Symposium, 2016.

Information Flow Control for Android Applications with Embedded WebPages, Julian Sexton. Master's Thesis, 2016.

Reasoning Tradeoffs in Languages with Enhanced Modularity Features, Jose Sanchez and Gary T. Leavens In 15th International Conference on Modularity, 2016.

Towards Modular Reasoning for Context-Oriented Programs, Tomoyuki Aotani and Gary T. Leavens. To appear in Formal Techniques for Java-like Programs, 2016.

Spekl: A Layered System for Specification Authoring, Sharing, and Usage, John L. Singleton and Gary T. Leavens. To appear in 4th IEEE International Workshop on Formal Methods Integration, 2016.

Specifying and Verifying Advanced Control Features, Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani. To appear in 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, 2016.

Inlined Information Flow Monitoring For JavaScript, Andrey Chudnov and David A. Naumann. In ACM Conference on Computer and Communications Security, 2015.

Towards Patterns for Heaps and Imperative Lambdas, David A. Naumann. To appear in Journal of Logical and Algebraic Methods in Programming, 2015

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning, Gary T. Leavens and David A. Naumann. In ACM Transactions on Programming Languages and Systems, 2015.

Information Flow Monitoring as Abstract Interpretation for Relational Logic, Andrey Chudnov, George Kuan and David A. Naumann. In IEEE Computer Security Foundations Symposium, 2014.

A Logical Analysis of Framing for Specifications with Pure Method Calls, Anindya Banerjee and David Naumann. In post-proceedings of Verified Software: Theories, Tools, Experiments, 2014.

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, Francois Dupressoir, Andrew D. Gordon, Jan Juerjens, and David Naumann. In Journal of Computer Security, 2014.

Analysis of Authentication and Key Establishment in Inter-generational Mobile Telephony, Chunyu Tang, David Naumann and Susanne Wetzel. In 4th International Symposium on Trust, Security and Privacy for Emerging Applications, 2013.

A Simple Semantics and Static Analysis for Stack Inspection, Anindya Banerjee and David Naumann. In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, 2013.

Local Reasoning for Global Invariants, Part I: Region Logic, Anindya Banerjee, David Naumann and Stan Rosenberg. Journal of the ACM, 2013.

Local Reasoning for Global Invariants, Part II: Dynamic Boundaries, Anindya Banerjee and David Naumann. Journal of the ACM, 2013.

Expressive declassification policies and modular static enforcement, Anindya Banerjee, David Naumann and Stan Rosenberg. In 29th IEEE Symposium on Security and Privacy, 2008, 339--353.

Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs, with Steve M. Shaner and Gary T. Leavens. In Object Oriented Programming, Languages, and Systems OOPSLA 2007, 351--368. Awarded Best Student Paper.

Allowing State Changes in Specifications, with Mike Barnett, Wolfram Schulte, and Qi Sun. Invited paper in International Conference on Emerging Trends in Information and Communication Security, 2006.