Spartan Jester: End-to-end Information Flow Control for Hybrid Android Applications,
Julian Sexton, Andrey Chudnov, David A. Naumann.
Hypercollecting Semantics and its Application to Static Analysis of Information Flow, Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, and Frederic Tronel. In
Relational Logic with Framing and Hypotheses, Anindya Banerjee, David A. Naumann, Mohammad Nikouei. In
Calculational Design of Information Flow Monitors, Mounir Assaf and David A. Naumann. In
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
Towards Modular Reasoning for Context-Oriented Programs, Tomoyuki Aotani and Gary T. Leavens. To appear in
Spekl: A Layered System for Specification Authoring, Sharing, and Usage, John L. Singleton and Gary T. Leavens. To appear in
Specifying and Verifying Advanced Control Features, Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani. To appear in
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
Information Flow Monitoring as Abstract Interpretation for Relational Logic, Andrey Chudnov, George Kuan and David A. Naumann. In
A Logical Analysis of Framing for Specifications with Pure Method Calls, Anindya Banerjee and David Naumann. In post-proceedings of
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols, Francois Dupressoir, Andrew D. Gordon, Jan Juerjens, and David Naumann. In
Analysis of Authentication and Key Establishment in Inter-generational Mobile Telephony, Chunyu Tang, David Naumann and Susanne Wetzel. In
A Simple Semantics and Static Analysis for Stack Inspection, Anindya Banerjee and David Naumann. In
Local Reasoning for Global Invariants, Part I: Region Logic, Anindya Banerjee, David Naumann and Stan Rosenberg.
Local Reasoning for Global Invariants, Part II: Dynamic Boundaries, Anindya Banerjee and David Naumann.
Expressive declassification policies and modular static enforcement, Anindya Banerjee, David Naumann and Stan Rosenberg. In
Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs, with Steve M. Shaner and Gary T. Leavens. In
Allowing State Changes in Specifications, with Mike Barnett, Wolfram Schulte, and Qi Sun. Invited paper in