David A. Naumann

According to our database1, David A. Naumann authored at least 86 papers between 1991 and 2019.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Whither Programs as Specifications.
CoRR, 2019

Typed-based Relaxed Noninterference for Free.
CoRR, 2019

Whither Specifications as Programs.
Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

2018
A Logical Analysis of Framing for Specifications with Pure Method Calls.
ACM Trans. Program. Lang. Syst., 2018

Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies.
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017
Spartan Jester: End-to-End Information Flow Control for Hybrid Android Applications.
Proceedings of the 2017 IEEE Security and Privacy Workshops, 2017

An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping.
Proceedings of the Engineering Trustworthy Software Systems - Third International School, 2017

Hypercollecting semantics and its application to static analysis of information flow.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016
Towards patterns for heaps and imperative lambdas.
J. Log. Algebr. Meth. Program., 2016

Relational Logic with Framing and Hypotheses: Technical Report.
CoRR, 2016

Hypercollecting Semantics and its Application to Static Analysis of Information Flow.
CoRR, 2016

Calculational Design of Information Flow Monitors (extended version).
CoRR, 2016

Specifying and Verifying Advanced Control Features.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Relational Logic with Framing and Hypotheses.
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

Calculational Design of Information Flow Monitors.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015
Behavioral Subtyping, Specification Inheritance, and Modular Reasoning.
ACM Trans. Program. Lang. Syst., 2015

Towards Patterns for Heaps and Imperative Lambdas.
CoRR, 2015

Inlined Information Flow Monitoring for JavaScript.
Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

2014
Guiding a general-purpose C verifier to prove cryptographic protocols.
Journal of Computer Security, 2014

A Logical Analysis of Framing for Specifications with Pure Method Calls.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

Information Flow Monitoring as Abstract Interpretation for Relational Logic.
Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

2013
State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings.
Proceedings of the Aliasing in Object-Oriented Programming. Types, 2013

Local Reasoning for Global Invariants, Part I: Region Logic.
J. ACM, 2013

Local Reasoning for Global Invariants, Part II: Dynamic Boundaries.
J. ACM, 2013

Analysis of authentication and key establishment in inter-generational mobile telephony.
IACR Cryptology ePrint Archive, 2013

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.
CoRR, 2013

A Simple Semantics and Static Analysis for Stack Inspection.
Proceedings of the Semantics, 2013

Analysis of Authentication and Key Establishment in Inter-generational Mobile Telephony.
Proceedings of the 10th IEEE International Conference on High Performance Computing and Communications & 2013 IEEE International Conference on Embedded and Ubiquitous Computing, 2013

Laws of Programming for References.
Proceedings of the Programming Languages and Systems - 11th Asian Symposium, 2013

2012
Refactoring and representation independence for class hierarchies.
Theor. Comput. Sci., 2012

Decision Procedures for Region Logic.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

2011
Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - [Extended Abstract].
Proceedings of the Security and Privacy in Communication Networks, 2011

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.
Proceedings of the 24th IEEE Computer Security Foundations Symposium, 2011

2010
Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients.
Proceedings of the Verified Software: Theories, 2010

Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions.
Proceedings of the Programming Languages and Systems, 2010

Refactoring and representation independence for class hierarchies: extended abstract.
Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, 2010

Information Flow Monitor Inlining.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

2009
Category Theoretic Models of Data Refinement.
Electr. Notes Theor. Comput. Sci., 2009

2008
Boogie Meets Regions: A Verification Experience Report.
Proceedings of the Verified Software: Theories, 2008

Expressive Declassification Policies and Modular Static Enforcement.
Proceedings of the 2008 IEEE Symposium on Security and Privacy (S&P 2008), 2008

Regional Logic for Local Reasoning about Global Invariants.
Proceedings of the ECOOP 2008, 2008

2007
Observational purity and encapsulation.
Theor. Comput. Sci., 2007

On assertion-based encapsulation for object invariants and simulations.
Formal Asp. Comput., 2007

Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model.
Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), 2007

Towards a logical account of declassification.
Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security, 2007

Modular verification of higher-order methods with mandatory calls specified by model programs.
Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2007

2006
Towards imperative modules: Reasoning about invariants and sharing of mutable state.
Theor. Comput. Sci., 2006

Deriving an Information Flow Checker and Certifying Compiler for Java.
Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P 2006), 2006

Allowing State Changes in Specifications.
Proceedings of the Emerging Trends in Information and Communication Security, 2006

From Coupling Relations to Mated Invariants for Checking Information Flow.
Proceedings of the Computer Security, 2006

Closing Internal Timing Channels by Transformation.
Proceedings of the Advances in Computer Science, 2006

2005
Stack-based access control and secure information flow.
J. Funct. Program., 2005

Ownership confinement ensures representation independence for object-oriented programs.
J. ACM, 2005

Modular Reasoning in Object-Oriented Programming.
Proceedings of the Verified Software: Theories, 2005

Verifying a Secure Information Flow Analyzer.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Observational Purity and Encapsulation.
Proceedings of the Fundamental Approaches to Software Engineering, 2005

State Based Ownership, Reentrance, and Encapsulation.
Proceedings of the ECOOP 2005, 2005

2004
Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language.
Proceedings of the Static Analysis, 11th International Symposium, 2004

Friends Need a Bit More: Maintaining Invariants Over Shared State.
Proceedings of the Mathematics of Program Construction, 7th International Conference, 2004

Towards Imperative Modules: Reasoning about Invariants and Sharing of Mutable State.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

Assertion-Based Encapsulation, Object Invariants and Simulations.
Proceedings of the Formal Methods for Components and Objects, 2004

History-Based Access Control and Secure Information Flow.
Proceedings of the Construction and Analysis of Safe, 2004

2003
CodeBLUE: a Bluetooth interactive dance club system.
Proceedings of the Global Telecommunications Conference, 2003

03411 Abstracts Collection - Language Based Security.
Proceedings of the Language-Based Security, 5.-10. October 2003, 2003

03411 Final Report - Language Based Security.
Proceedings of the Language-Based Security, 5.-10. October 2003, 2003

Using Access Control for Secure Information Flow in a Java-like Language.
Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW-16 2003), 30 June, 2003

2002
Soundness of data refinement for a higher-order imperative language.
Theor. Comput. Sci., 2002

Ownership Confinement Ensures Representation Independence for Object-Oriented Programs
CoRR, 2002

Representation independence, confinement and access control [extended abstract].
Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Forward Simulation for Data Refinement of Classes.
Proceedings of the FME 2002: Formal Methods, 2002

Secure Information Flow and Pointer Confinement in a Java-like Language.
Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW-15 2002), 2002

2001
Predicate transformer semantics of a higher-order imperative language with record subtyping.
Sci. Comput. Program., 2001

Calculating sharp adaptation rules.
Inf. Process. Lett., 2001

Ideal Models for Pointwise Relational and State-Free Imperative Programming.
Proceedings of the 3rd international ACM SIGPLAN conference on Principles and practice of declarative programming, 2001

2000
A Weakest Precondition Semantics for Refinement of Object-Oriented Programs.
IEEE Trans. Software Eng., 2000

1999
A Weakest Precondition Semantics for an Object-Oriented Language of Refinement.
Proceedings of the FM'99 - Formal Methods, 1999

1998
A Categorical Model for Higher Order Imperative Programming.
Mathematical Structures in Computer Science, 1998

Towards squiggly refinement algebra.
Proceedings of the Programming Concepts and Methods, 1998

Beyond Fun: Order and Membership in Polytypic Imperative Programming.
Proceedings of the Mathematics of Program Construction, 1998

1995
Predicate Transformers and Higher-Order Programs.
Theor. Comput. Sci., 1995

Data Refinement, Call by Value and Higher Order Programs.
Formal Asp. Comput., 1995

1994
A Recursion Theorem for Predicate Transformers on Inductive Data Types.
Inf. Process. Lett., 1994

Derivation of programs for freshmen.
Proceedings of the 25th SIGCSE Technical Symposium on Computer Science Education, 1994

Predicate Transformer Semantics of an Oberon-Like Language.
Proceedings of the Programming Concepts, 1994

On the Essence of Oberon.
Proceedings of the Programming Languages and System Architectures, 1994

1991
A Commonsense Management Model.
IEEE Software, 1991


  Loading...