David A. Naumann

J. Comput. Secur., 2023

Toward Tool-Independent Summaries for Symbolic Execution (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2023

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2023

Alignment complete relational Hoare logics for some and all.

[BibT_eX]

[DOI]

CoRR, 2023

The WhyRel Prototype for Relational Verification.

[BibT_eX]

[DOI]

CoRR, 2023

The WhyRel Prototype for Modular Relational Verification of Pointer Programs.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Toward Tool-Independent Summaries for Symbolic Execution.

[BibT_eX]

[DOI]

Proceedings of the 37th European Conference on Object-Oriented Programming, 2023

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications.

[BibT_eX]

[DOI]

Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security, 2023

2022

A Relational Program Logic with Data Abstraction and Dynamic Framing.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., December, 2022

Making Relational Hoare Logic Alignment Complete.

[BibT_eX]

[DOI]

CoRR, 2022

2021

Alignment Completeness for Relational Hoare Logics.

[BibT_eX]

[DOI]

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Verified sequential Malloc/Free.

[BibT_eX]

[DOI]

Andrew W. Appel

Proceedings of the ISMM '20: 2020 ACM SIGPLAN International Symposium on Memory Management, 2020

Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles, 2020

Type-Based Declassification for Free.

[BibT_eX]

[DOI]

Minh Ngo

Tamara Rezk

Proceedings of the Formal Methods and Software Engineering, 2020

2019

Data Abstraction and Relational Program Logic.

[BibT_eX]

[DOI]

CoRR, 2019

Whither Programs as Specifications.

[BibT_eX]

[DOI]

CoRR, 2019

Typed-based Relaxed Noninterference for Free.

[BibT_eX]

[DOI]

Minh Ngo

Tamara Rezk

CoRR, 2019

Whither Specifications as Programs.

[BibT_eX]

[DOI]

Minh Ngo

Proceedings of the Unifying Theories of Programming - 7th International Symposium, 2019

2018

A Logical Analysis of Framing for Specifications with Pure Method Calls.

[BibT_eX]

[DOI]

Mohammad Nikouei

ACM Trans. Program. Lang. Syst., 2018

Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017

Spartan Jester: End-to-End Information Flow Control for Hybrid Android Applications.

[BibT_eX]

[DOI]

Julian Sexton

Proceedings of the 2017 IEEE Security and Privacy Workshops, 2017

An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping.

[BibT_eX]

[DOI]

Gary T. Leavens

Proceedings of the Engineering Trustworthy Software Systems - Third International School, 2017

Hypercollecting semantics and its application to static analysis of information flow.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

Towards patterns for heaps and imperative lambdas.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2016

Relational Logic with Framing and Hypotheses: Technical Report.

[BibT_eX]

[DOI]

Mohammad Nikouei

CoRR, 2016

Calculational Design of Information Flow Monitors (extended version).

[BibT_eX]

[DOI]

Mounir Assaf

CoRR, 2016

Specifying and Verifying Advanced Control Features.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

Relational Logic with Framing and Hypotheses.

[BibT_eX]

[DOI]

Mohammad Nikouei

Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016

Calculational Design of Information Flow Monitors.

[BibT_eX]

[DOI]

Mounir Assaf

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning.

[BibT_eX]

[DOI]

Gary T. Leavens

ACM Trans. Program. Lang. Syst., 2015

Inlined Information Flow Monitoring for JavaScript.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

2014

Guiding a general-purpose C verifier to prove cryptographic protocols.

[BibT_eX]

[DOI]

J. Comput. Secur., 2014

A Logical Analysis of Framing for Specifications with Pure Method Calls.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

Information Flow Monitoring as Abstract Interpretation for Relational Logic.

[BibT_eX]

[DOI]

George Kuan

Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

2013

State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings.

[BibT_eX]

[DOI]

Proceedings of the Aliasing in Object-Oriented Programming. Types, 2013

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

[BibT_eX]

[DOI]

J. ACM, 2013

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

[BibT_eX]

[DOI]

J. ACM, 2013

Analysis of authentication and key establishment in inter-generational mobile telephony.

[BibT_eX]

[DOI]

Chunyu Tang

Susanne Wetzel

IACR Cryptol. ePrint Arch., 2013

A Simple Semantics and Static Analysis for Stack Inspection.

[BibT_eX]

[DOI]

Proceedings of the Semantics, 2013

Laws of Programming for References.

[BibT_eX]

[DOI]

Giovanny Lucero

Augusto Sampaio

Proceedings of the Programming Languages and Systems - 11th Asian Symposium, 2013

2012

Refactoring and representation independence for class hierarchies.

[BibT_eX]

[DOI]

Augusto Sampaio

Leila Silva

Theor. Comput. Sci., 2012

Decision Procedures for Region Logic.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

2011

Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - [Extended Abstract].

[BibT_eX]

[DOI]

Chunyu Tang

Susanne Wetzel

Proceedings of the Security and Privacy in Communication Networks, 2011

2010

Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2010

Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2010

Refactoring and representation independence for class hierarchies: extended abstract.

[BibT_eX]

[DOI]

Leila Silva

Augusto Sampaio

Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, 2010

Information Flow Monitor Inlining.

[BibT_eX]

[DOI]

Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

2008

Boogie Meets Regions: A Verification Experience Report.

[BibT_eX]

[DOI]

Michael Barnett

Proceedings of the Verified Software: Theories, 2008

Expressive Declassification Policies and Modular Static Enforcement.

[BibT_eX]

[DOI]

Proceedings of the 2008 IEEE Symposium on Security and Privacy (SP 2008), 2008

Regional Logic for Local Reasoning about Global Invariants.

[BibT_eX]

[DOI]

Proceedings of the ECOOP 2008, 2008

2007

Observational purity and encapsulation.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

On assertion-based encapsulation for object invariants and simulations.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2007

Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model.

[BibT_eX]

[DOI]

Marco Pistoia

Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), 2007

Towards a logical account of declassification.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Steve M. Shaner

Gary T. Leavens

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.

[BibT_eX]

[DOI]

Michael Barnett

Theor. Comput. Sci., 2006

Category Theoretic Models of Data Refinement.

[BibT_eX]

[DOI]

Michael Johnson

John Power

Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, 2006

Deriving an Information Flow Checker and Certifying Compiler for Java.

[BibT_eX]

[DOI]

Gilles Barthe

Tamara Rezk

Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P 2006), 2006

Allowing State Changes in Specifications.

[BibT_eX]

[DOI]

Proceedings of the Emerging Trends in Information and Communication Security, 2006

From Coupling Relations to Mated Invariants for Checking Information Flow.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 2006

Closing Internal Timing Channels by Transformation.

[BibT_eX]

[DOI]

Proceedings of the Advances in Computer Science, 2006

2005

Stack-based access control and secure information flow.

[BibT_eX]

[DOI]

J. Funct. Program., 2005

Ownership confinement ensures representation independence for object-oriented programs.

[BibT_eX]

[DOI]

J. ACM, 2005

Modular Reasoning in Object-Oriented Programming.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Verifying a Secure Information Flow Analyzer.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

State Based Ownership, Reentrance, and Encapsulation.

[BibT_eX]

[DOI]

Proceedings of the ECOOP 2005, 2005

2004

Modular and Constraint-Based Information Flow Inference for an Object-Oriented Language.

[BibT_eX]

[DOI]

Qi Sun

Proceedings of the Static Analysis, 11th International Symposium, 2004

Friends Need a Bit More: Maintaining Invariants Over Shared State.

[BibT_eX]

[DOI]

Michael Barnett

Proceedings of the Mathematics of Program Construction, 7th International Conference, 2004

History-Based Access Control and Secure Information Flow.

[BibT_eX]

[DOI]

Proceedings of the Construction and Analysis of Safe, 2004

2003

CodeBLUE: a Bluetooth interactive dance club system.

[BibT_eX]

[DOI]

Proceedings of the Global Telecommunications Conference, 2003

03411 Abstracts Collection - Language Based Security.

[BibT_eX]

[DOI]

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

03411 Final Report - Language Based Security.

[BibT_eX]

[DOI]

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

Using Access Control for Secure Information Flow in a Java-like Language.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2002

Representation independence, confinement and access control [extended abstract].

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Ana Cavalcanti

Proceedings of the FME 2002: Formal Methods, 2002

Secure Information Flow and Pointer Confinement in a Java-like Language.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2001

Calculating sharp adaptation rules.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2001

Ideal Models for Pointwise Relational and State-Free Imperative Programming.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Ana Cavalcanti

IEEE Trans. Software Eng., 2000

1999

A Weakest Precondition Semantics for an Object-Oriented Language of Refinement.

[BibT_eX]

[DOI]

Ana Cavalcanti

Proceedings of the FM'99 - Formal Methods, 1999

1998

A Categorical Model for Higher Order Imperative Programming.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1998

Towards squiggly refinement algebra.

[BibT_eX]

Proceedings of the Programming Concepts and Methods, 1998

Beyond Fun: Order and Membership in Polytypic Imperative Programming.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 1998

1995

Predicate Transformers and Higher-Order Programs.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

Data Refinement, Call by Value and Higher Order Programs.

[BibT_eX]

[DOI]

Formal Aspects Comput., 1995

1994

A Recursion Theorem for Predicate Transformers on Inductive Data Types.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1994

Derivation of programs for freshmen.

[BibT_eX]

[DOI]

Proceedings of the 25th SIGCSE Technical Symposium on Computer Science Education, 1994

Predicate Transformer Semantics of an Oberon-Like Language.

[BibT_eX]

Proceedings of the Programming Concepts, 1994

On the Essence of Oberon.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and System Architectures, 1994

1991

A Commonsense Management Model.

[BibT_eX]

[DOI]

Raymond T. Yeh