2024
A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs.
CoRR, 2024
2023
Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning.
Proc. ACM Program. Lang., 2023
Alignment complete relational Hoare logics for some and all.
CoRR, 2023
The WhyRel Prototype for Relational Verification.
CoRR, 2023
Inductive Reasoning for Coinductive Types.
CoRR, 2023
The WhyRel Prototype for Modular Relational Verification of Pointer Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023
2022
A Relational Program Logic with Data Abstraction and Dynamic Framing.
ACM Trans. Program. Lang. Syst., December, 2022
Making Relational Hoare Logic Alignment Complete.
CoRR, 2022
2021
On algebraic abstractions for concurrent separation logics.
Proc. ACM Program. Lang., 2021
Navigating the Seismic Shift of Post-Moore Computer Systems Design.
IEEE Micro, 2021
A formal proof of PAC learnability for decision stumps.
Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021
2020
A Theory of Slicing for Imperative Probabilistic Programs.
ACM Trans. Program. Lang. Syst., 2020
Verification of ML Systems via Reparameterization.
CoRR, 2020
2019
Specifying concurrent programs in separation logic: morphisms and simulations.
Proc. ACM Program. Lang., 2019
Data Abstraction and Relational Program Logic.
CoRR, 2019
2018
A Logical Analysis of Framing for Specifications with Pure Method Calls.
ACM Trans. Program. Lang. Syst., 2018
2017
Concurrent Data Structures Linked in Time (Artifact).
Dagstuhl Artifacts Ser., 2017
A Semantics for Probabilistic Control-Flow Graphs.
CoRR, 2017
Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources.
CoRR, 2017
Concurrent Data Structures Linked in Time.
Proceedings of the 31st European Conference on Object-Oriented Programming, 2017
2016
Relational Logic with Framing and Hypotheses: Technical Report.
CoRR, 2016
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects.
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 2016
Relational Logic with Framing and Hypotheses.
Proceedings of the 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2016
A Theory of Slicing for Probabilistic Control Flow Graphs.
Proceedings of the Foundations of Software Science and Computation Structures, 2016
2015
Mechanized verification of fine-grained concurrent programs.
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015
Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.
Proceedings of the Programming Languages and Systems, 2015
2014
On Automation in the Verification of Software Barriers: Experience Report.
J. Autom. Reason., 2014
A Logical Analysis of Framing for Specifications with Pure Method Calls.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014
Modular reasoning about heap paths via effectively propositional formulas.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014
2013
State Based Encapsulation for Modular Reasoning about Behavior-Preserving Refactorings.
Proceedings of the Aliasing in Object-Oriented Programming. Types, 2013
Dependent Type Theory for Verification of Information Flow and Access Control Policies.
ACM Trans. Program. Lang. Syst., 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
A Simple Semantics and Static Analysis for Stack Inspection.
Proceedings of the Semantics, 2013
Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures.
Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013
Effectively-Propositional Reasoning about Reachability in Linked Data Structures.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013
2012
Decision Procedures for Region Logic.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012
Verification of software barriers.
Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2012
Programming Paradigm Driven Heap Analysis.
Proceedings of the Compiler Construction - 21st International Conference, 2012
2011
Modelling declassification policies using abstract domain completeness.
Math. Struct. Comput. Sci., 2011
Verification of Information Flow and Access Control Policies with Dependent Types.
Proceedings of the 32nd IEEE Symposium on Security and Privacy, 2011
Modular Verification of Object-Based Programs - Abstract of Invited Talk.
Proceedings of the Formal Verification of Object-Oriented Software, 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
2009
A language for information flow: dynamic tracking in multiple interdependent dimensions.
Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, 2009
Merlin: specification inference for explicit information flow problems.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009
Semantics and Enforcement of Expressive Information Flow Policies.
Proceedings of the Formal Aspects in Security and Trust, 6th International Workshop, 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 (SP 2008), 2008
Formal Techniques for Java-Like Programs.
Proceedings of the Object-Oriented Technology. ECOOP 2008 Workshop Reader, 2008
Regional Logic for Local Reasoning about Global Invariants.
Proceedings of the ECOOP 2008, 2008
2007
A new foundation for control dependence and slicing for modern program structures.
ACM Trans. Program. Lang. Syst., 2007
A logic for information flow analysis with an application to forward slicing of simple imperative programs.
Sci. Comput. Program., 2007
What You Lose is What You Leak: Information Leakage in Declassification Policies.
Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, 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
Verification condition generation for conditional information flow.
Proceedings of the 2007 ACM workshop on Formal methods in security engineering, 2007
2006
A logic for information flow in object-oriented programs.
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006
Automata-Based Confidentiality Monitoring.
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
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
Information Flow Analysis in Logical Form.
Proceedings of the Static Analysis, 11th International Symposium, 2004
History-Based Access Control and Secure Information Flow.
Proceedings of the Construction and Analysis of Safe, 2004
2003
Modular Control-Flow Analysis with Rank 2 Intersection Types.
Math. Struct. Comput. Sci., 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
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
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
Design and Correctness of Program Transformations Based on Control-Flow Analysis.
Proceedings of the Theoretical Aspects of Computer Software, 4th International Symposium, 2001
1999
A Core Calculus of Dependency.
Proceedings of the POPL '99, 1999
Region Analysis and the Polymorphic Lambda Calculus.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999
1998
Stackability in the Simply-Typed Call-by-Value lambda Calculus.
Sci. Comput. Program., 1998
1997
A Modular, Polyvariant, and Type-Based Closure Analysis.
Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997
1993
A Categorical Interpretation of Landin's Correspondence Principle.
Proceedings of the Mathematical Foundations of Programming Semantics, 1993