David A. Naumann

112 papers A* 7A 12B 7C 4Journal 44Unranked 33

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Alignment complete relational Hoare logics for some and all. Log. Methods Comput. Sci. Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
2025	J	`jnl`	Forall-Exists Relational Verification by Filtering to Forall-Forall. CoRR Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
2024	—	`conf`	Verifying a C Implementation of Derecho's Coordination Mechanism Using VST and Coq. NFM Ramana Nagasamudram, Lennart Beringer, Ken Birman, Mae Milano, David A. Naumann
2023	J	`jnl`	Alignment complete relational Hoare logics for some and all. CoRR Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
2023	J	`jnl`	An Algebra of Alignment for Relational Verification. Proc. ACM Program. Lang. Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, Minh Ngo
2023	J	`jnl`	Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version). CoRR Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann
2023	A*	`conf`	Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. CCS Toby Murray, Mukesh Tiwari, Gidon Ernst, David A. Naumann
2023	J	`jnl`	Special issue: 35th IEEE Computer Security Symposium - CSF 2022. J. Comput. Secur. Stefano Calzavara, David A. Naumann
2023	—	`conf`	The WhyRel Prototype for Modular Relational Verification of Pointer Programs. TACAS (2) Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
2023	J	`jnl`	The WhyRel Prototype for Relational Verification. CoRR Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
2023	J	`jnl`	Toward Tool-Independent Summaries for Symbolic Execution (Artifact). Dagstuhl Artifacts Ser. Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, José Fragoso Santos
2023	A	`conf`	Toward Tool-Independent Summaries for Symbolic Execution. ECOOP Frederico Ramos, Nuno Sabino, Pedro Adão, David A. Naumann, José Fragoso Santos
2022	J	`jnl`	A Relational Program Logic with Data Abstraction and Dynamic Framing. ACM Trans. Program. Lang. Syst. Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, Mohammad Nikouei
2022	J	`jnl`	An algebra of alignment for relational verification. CoRR Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, Minh Ngo
2022	J	`jnl`	Making Relational Hoare Logic Alignment Complete. CoRR Anindya Banerjee, Ramana Nagasamudram, David A. Naumann
2021	A*	`conf`	Alignment Completeness for Relational Hoare Logics. LICS Ramana Nagasamudram, David A. Naumann
2021	J	`jnl`	Alignment Completeness for Relational Hoare Logics. CoRR Ramana Nagasamudram, David A. Naumann
2020	—	`conf`	Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. ISoLA (2) David A. Naumann
2020	J	`jnl`	Thirty-seven years of relational Hoare logic: remarks on its principles and history. CoRR David A. Naumann
2020	C	`conf`	Type-Based Declassification for Free. ICFEM Minh Ngo, David A. Naumann, Tamara Rezk
2020	C	`conf`	Verified sequential Malloc/Free. ISMM Andrew W. Appel, David A. Naumann
2019	J	`jnl`	Data Abstraction and Relational Program Logic. CoRR Anindya Banerjee, Ramana Nagasamudram, David A. Naumann, Mohammad Nikouei
2019	J	`jnl`	Typed-based Relaxed Noninterference for Free. CoRR Minh Ngo, David A. Naumann, Tamara Rezk
2019	J	`jnl`	Whither Programs as Specifications. CoRR David A. Naumann
2019	—	`conf`	Whither Specifications as Programs. UTP David A. Naumann, Minh Ngo
2018	J	`jnl`	A Logical Analysis of Framing for Specifications with Pure Method Calls. ACM Trans. Program. Lang. Syst. Anindya Banerjee, David A. Naumann, Mohammad Nikouei
2018	A	`conf`	Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies. CSF Andrey Chudnov, David A. Naumann
2017	—	`conf`	An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping. SETSS Gary T. Leavens, David A. Naumann
2017	A*	`conf`	Hypercollecting semantics and its application to static analysis of information flow. POPL Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel
2017	—	`conf`	Spartan Jester: End-to-End Information Flow Control for Hybrid Android Applications. IEEE Symposium on Security and Privacy Workshops Julian Sexton, Andrey Chudnov, David A. Naumann
2016	J	`jnl`	Calculational Design of Information Flow Monitors (extended version). CoRR Mounir Assaf, David A. Naumann
2016	A	`conf`	Calculational Design of Information Flow Monitors. CSF Mounir Assaf, David A. Naumann
2016	J	`jnl`	Hypercollecting Semantics and its Application to Static Analysis of Information Flow. CoRR Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel
2016	—	`conf`	Relational Logic with Framing and Hypotheses. FSTTCS Anindya Banerjee, David A. Naumann, Mohammad Nikouei
2016	J	`jnl`	Relational Logic with Framing and Hypotheses: Technical Report. CoRR Anindya Banerjee, David A. Naumann, Mohammad Nikouei
2016	—	`conf`	Specifying and Verifying Advanced Control Features. ISoLA (2) Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani
2016	J	`jnl`	Towards patterns for heaps and imperative lambdas. J. Log. Algebraic Methods Program. David A. Naumann
2015	J	`jnl`	Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. ACM Trans. Program. Lang. Syst. Gary T. Leavens, David A. Naumann
2015	A*	`conf`	Inlined Information Flow Monitoring for JavaScript. CCS Andrey Chudnov, David A. Naumann
2015	J	`jnl`	Towards Patterns for Heaps and Imperative Lambdas. CoRR David A. Naumann
2015	—	`ed.`	Unifying Theories of Programming - 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers UTP David A. Naumann
2014	—	`conf`	A Logical Analysis of Framing for Specifications with Pure Method Calls. VSTTE Anindya Banerjee, David A. Naumann
2014	J	`jnl`	Guiding a general-purpose C verifier to prove cryptographic protocols. J. Comput. Secur. François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
2014	A	`conf`	Information Flow Monitoring as Abstract Interpretation for Relational Logic. CSF Andrey Chudnov, George Kuan, David A. Naumann
2013	—	`conf`	A Simple Semantics and Static Analysis for Stack Inspection. Festschrift for Dave Schmidt Anindya Banerjee, David A. Naumann
2013	—	`conf`	Analysis of Authentication and Key Establishment in Inter-generational Mobile Telephony. HPCC/EUC Chunyu Tang, David A. Naumann, Susanne Wetzel
2013	J	`jnl`	Analysis of authentication and key establishment in inter-generational mobile telephony. IACR Cryptol. ePrint Arch. Chunyu Tang, David A. Naumann, Susanne Wetzel
2013	J	`jnl`	Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. CoRR François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
2013	B	`conf`	Laws of Programming for References. APLAS Giovanny Lucero, David A. Naumann, Augusto Sampaio
2013	J	`jnl`	Local Reasoning for Global Invariants, Part I: Region Logic. J. ACM Anindya Banerjee, David A. Naumann, Stan Rosenberg
2013	J	`jnl`	Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. J. ACM Anindya Banerjee, David A. Naumann
2013	—	`ch.`	State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings. Aliasing in Object-Oriented Programming Anindya Banerjee, David A. Naumann
2012	B	`conf`	Decision Procedures for Region Logic. VMCAI Stan Rosenberg, Anindya Banerjee, David A. Naumann
2012	—	`ed.`	Formal Methods: Foundations and Applications - 15th Brazilian Symposium, SBMF 2012, Natal, Brazil, September 23-28, 2012. Proceedings SBMF Rohit Gheyi, David A. Naumann
2012	J	`jnl`	Refactoring and representation independence for class hierarchies. Theor. Comput. Sci. David A. Naumann, Augusto Sampaio, Leila Silva
2011	A	`conf`	Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. CSF François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
2011	C	`conf`	Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - [Extended Abstract]. SecureComm Chunyu Tang, David A. Naumann, Susanne Wetzel
2010	A	`conf`	Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions. ESOP David A. Naumann, Anindya Banerjee
2010	A	`conf`	Information Flow Monitor Inlining. CSF Andrey Chudnov, David A. Naumann
2010	—	`conf`	Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients. VSTTE Stan Rosenberg, Anindya Banerjee, David A. Naumann
2010	—	`conf`	Refactoring and representation independence for class hierarchies: extended abstract. FTfJP@ECOOP Leila Silva, David A. Naumann, Augusto Sampaio
2009	—	`ed.`	Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, PLAS 2009, Dublin, Ireland, 15-21 June, 2009 PLAS Stephen Chong, David A. Naumann
2008	—	`conf`	Boogie Meets Regions: A Verification Experience Report. VSTTE Anindya Banerjee, Michael Barnett, David A. Naumann
2008	A*	`conf`	Expressive Declassification Policies and Modular Static Enforcement. SP Anindya Banerjee, David A. Naumann, Stan Rosenberg
2008	A	`conf`	Regional Logic for Local Reasoning about Global Invariants. ECOOP Anindya Banerjee, David A. Naumann, Stan Rosenberg
2007	—	`conf`	Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model. S&P Marco Pistoia, Anindya Banerjee, David A. Naumann
2007	A	`conf`	Modular verification of higher-order methods with mandatory calls specified by model programs. OOPSLA Steve M. Shaner, Gary T. Leavens, David A. Naumann
2007	J	`jnl`	Observational purity and encapsulation. Theor. Comput. Sci. David A. Naumann
2007	J	`jnl`	On assertion-based encapsulation for object invariants and simulations. Formal Aspects Comput. David A. Naumann
2007	—	`conf`	Towards a logical account of declassification. PLAS Anindya Banerjee, David A. Naumann, Stan Rosenberg
2006	—	`conf`	Allowing State Changes in Specifications. ETRICS Michael Barnett, David A. Naumann, Wolfram Schulte, Qi Sun
2006	—	`conf`	Category Theoretic Models of Data Refinement. MFCSIT Michael Johnson, David A. Naumann, John Power
2006	—	`conf`	Closing Internal Timing Channels by Transformation. ASIAN Alejandro Russo, John Hughes, David A. Naumann, Andrei Sabelfeld
2006	—	`conf`	Deriving an Information Flow Checker and Certifying Compiler for Java. S&P Gilles Barthe, Tamara Rezk, David A. Naumann
2006	A	`conf`	From Coupling Relations to Mated Invariants for Checking Information Flow. ESORICS David A. Naumann
2006	J	`jnl`	Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theor. Comput. Sci. David A. Naumann, Michael Barnett
2005	—	`ed.`	Language-Based Security, 5.-10. October 2003 Language-Based Security Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld
2005	—	`conf`	Modular Reasoning in Object-Oriented Programming. VSTTE David A. Naumann
2005	B	`conf`	Observational Purity and Encapsulation. FASE David A. Naumann
2005	J	`jnl`	Ownership confinement ensures representation independence for object-oriented programs. J. ACM Anindya Banerjee, David A. Naumann
2005	J	`jnl`	Stack-based access control and secure information flow. J. Funct. Program. Anindya Banerjee, David A. Naumann
2005	A	`conf`	State Based Ownership, Reentrance, and Encapsulation. ECOOP Anindya Banerjee, David A. Naumann
2005	—	`conf`	Verifying a Secure Information Flow Analyzer. TPHOLs David A. Naumann
2004	—	`conf`	Assertion-Based Encapsulation, Object Invariants and Simulations. FMCO David A. Naumann
2004	B	`conf`	Friends Need a Bit More: Maintaining Invariants Over Shared State. MPC Michael Barnett, David A. Naumann
2004	—	`conf`	History-Based Access Control and Secure Information Flow. CASSIS Anindya Banerjee, David A. Naumann
2004	B	`conf`	Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language. SAS Qi Sun, Anindya Banerjee, David A. Naumann
2004	A*	`conf`	Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State. LICS David A. Naumann, Michael Barnett
2003	—	`conf`	03411 Abstracts Collection - Language Based Security. Language Based Security Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld
2003	—	`conf`	03411 Final Report - Language Based Security. Language Based Security Anindya Banerjee, Heiko Mantel, David A. Naumann, Andrei Sabelfeld
2003	B	`conf`	CodeBLUE: a Bluetooth interactive dance club system. GLOBECOM Dennis Hromin, Michael Chladil, Natalie Vanatta, David A. Naumann, Susanne Wetzel, Farooq Anjum, Ravi Jain
2003	—	`conf`	Using Access Control for Secure Information Flow in a Java-like Language. CSFW Anindya Banerjee, David A. Naumann
2002	—	`conf`	Forward Simulation for Data Refinement of Classes. FME Ana Cavalcanti, David A. Naumann
2002	J	`jnl`	Ownership Confinement Ensures Representation Independence for Object-Oriented Programs CoRR Anindya Banerjee, David A. Naumann
2002	A*	`conf`	Representation independence, confinement and access control [extended abstract]. POPL Anindya Banerjee, David A. Naumann
2002	—	`conf`	Secure Information Flow and Pointer Confinement in a Java-like Language. CSFW Anindya Banerjee, David A. Naumann
2002	J	`jnl`	Soundness of data refinement for a higher-order imperative language. Theor. Comput. Sci. David A. Naumann
2001	J	`jnl`	Calculating sharp adaptation rules. Inf. Process. Lett. David A. Naumann
2001	C	`conf`	Ideal Models for Pointwise Relational and State-Free Imperative Programming. PPDP David A. Naumann
2001	J	`jnl`	Predicate transformer semantics of a higher-order imperative language with record subtyping. Sci. Comput. Program. David A. Naumann
2000	J	`jnl`	A Weakest Precondition Semantics for Refinement of Object-Oriented Programs. IEEE Trans. Software Eng. Ana Cavalcanti, David A. Naumann
1999	—	`conf`	A Weakest Precondition Semantics for an Object-Oriented Language of Refinement. World Congress on Formal Methods Ana Cavalcanti, David A. Naumann
1998	J	`jnl`	A Categorical Model for Higher Order Imperative Programming. Math. Struct. Comput. Sci. David A. Naumann
1998	B	`conf`	Beyond Fun: Order and Membership in Polytypic Imperative Programming. MPC David A. Naumann
1998	—	`conf`	Towards squiggly refinement algebra. PROCOMET David A. Naumann
1995	J	`jnl`	Data Refinement, Call by Value and Higher Order Programs. Formal Aspects Comput. David A. Naumann
1995	J	`jnl`	Predicate Transformers and Higher-Order Programs. Theor. Comput. Sci. David A. Naumann
1994	J	`jnl`	A Recursion Theorem for Predicate Transformers on Inductive Data Types. Inf. Process. Lett. David A. Naumann
1994	A	`conf`	Derivation of programs for freshmen. SIGCSE Richard T. Denman, David A. Naumann, Walter Potter, Gary Richter
1994	—	`conf`	On the Essence of Oberon. Programming Languages and System Architectures David A. Naumann
1994	—	`conf`	Predicate Transformer Semantics of an Oberon-Like Language. PROCOMET David A. Naumann
1991	J	`jnl`	A Commonsense Management Model. IEEE Softw. Raymond T. Yeh, David A. Naumann, Roland T. Mittermeir, Reinhard A. Schlemmer, William S. Gilmore, George E. Sumrall, John T. Lebaron