Anindya Banerjee

Proc. ACM Program. Lang., 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

Inductive Reasoning for Coinductive Types.

[BibT_eX]

[DOI]

Alexander Bagnall

Gordon Stewart

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

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

On algebraic abstractions for concurrent separation logics.

[BibT_eX]

[DOI]

Frantisek Farka

Ignacio Fábregas

Proc. ACM Program. Lang., 2021

Navigating the Seismic Shift of Post-Moore Computer Systems Design.

[BibT_eX]

[DOI]

IEEE Micro, 2021

A formal proof of PAC learnability for decision stumps.

[BibT_eX]

[DOI]

Joseph Tassarotti

Koundinya Vajjha

Jean-Baptiste Tristan

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.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2020

Verification of ML Systems via Reparameterization.

[BibT_eX]

[DOI]

Jean-Baptiste Tristan

CoRR, 2020

2019

Specifying concurrent programs in separation logic: morphisms and simulations.

[BibT_eX]

[DOI]

Ignacio Fábregas

Proc. ACM Program. Lang., 2019

Data Abstraction and Relational Program Logic.

[BibT_eX]

[DOI]

CoRR, 2019

2018

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

[BibT_eX]

[DOI]

Mohammad Nikouei

ACM Trans. Program. Lang. Syst., 2018

2017

Concurrent Data Structures Linked in Time (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2017

A Semantics for Probabilistic Control-Flow Graphs.

[BibT_eX]

[DOI]

CoRR, 2017

Subjective Simulation as a Notion of Morphism for Composing Concurrent Resources.

[BibT_eX]

[DOI]

CoRR, 2017

Concurrent Data Structures Linked in Time.

[BibT_eX]

[DOI]

Proceedings of the 31st European Conference on Object-Oriented Programming, 2017

2016

Relational Logic with Framing and Hypotheses: Technical Report.

[BibT_eX]

[DOI]

Mohammad Nikouei

CoRR, 2016

Hoare-style specifications as correctness conditions for non-linearizable concurrent objects.

[BibT_eX]

[DOI]

Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, 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

A Theory of Slicing for Probabilistic Control Flow Graphs.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2016

2015

Mechanized verification of fine-grained concurrent programs.

[BibT_eX]

[DOI]

Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015

Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2015

2014

On Automation in the Verification of Software Barriers: Experience Report.

[BibT_eX]

[DOI]

Alexander Malkis

J. Autom. Reason., 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

Modular reasoning about heap paths via effectively propositional formulas.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

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

Dependent Type Theory for Verification of Information Flow and Access Control Policies.

[BibT_eX]

[DOI]

Deepak Garg

ACM Trans. Program. Lang. Syst., 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

A Simple Semantics and Static Analysis for Stack Inspection.

[BibT_eX]

[DOI]

Proceedings of the Semantics, 2013

Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures.

[BibT_eX]

[DOI]

Gordon Stewart

Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming, 2013

Effectively-Propositional Reasoning about Reachability in Linked Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

2012

Decision Procedures for Region Logic.

[BibT_eX]

[DOI]

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

Verification of software barriers.

[BibT_eX]

[DOI]

Alexander Malkis

Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2012

Programming Paradigm Driven Heap Analysis.

[BibT_eX]

[DOI]

Mark Marron

Ondrej Lhoták

Proceedings of the Compiler Construction - 21st International Conference, 2012

2011

Modelling declassification policies using abstract domain completeness.

[BibT_eX]

[DOI]

Isabella Mastroeni

Math. Struct. Comput. Sci., 2011

Verification of Information Flow and Access Control Policies with Dependent Types.

[BibT_eX]

[DOI]

Deepak Garg

Proceedings of the 32nd IEEE Symposium on Security and Privacy, 2011

Modular Verification of Object-Based Programs - Abstract of Invited Talk.

[BibT_eX]

[DOI]

Proceedings of the Formal Verification of Object-Oriented Software, 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

2009

A language for information flow: dynamic tracking in multiple interdependent dimensions.

[BibT_eX]

[DOI]

Avraham Shinnar

Marco Pistoia

Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security, 2009

Merlin: specification inference for explicit information flow problems.

[BibT_eX]

[DOI]

Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Semantics and Enforcement of Expressive Information Flow Policies.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects in Security and Trust, 6th International Workshop, 2009

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

Formal Techniques for Java-Like Programs.

[BibT_eX]

[DOI]

Proceedings of the Object-Oriented Technology. ECOOP 2008 Workshop Reader, 2008

Regional Logic for Local Reasoning about Global Invariants.

[BibT_eX]

[DOI]

Venkatesh Prasad Ranganath

Proceedings of the ECOOP 2008, 2008

2007

A new foundation for control dependence and slicing for modern program structures.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2007

A logic for information flow analysis with an application to forward slicing of simple imperative programs.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2007

What You Lose is What You Leak: Information Leakage in Declassification Policies.

[BibT_eX]

[DOI]

Roberto Giacobazzi

Isabella Mastroeni

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.

[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

Verification condition generation for conditional information flow.

[BibT_eX]

[DOI]

Proceedings of the 2007 ACM workshop on Formal methods in security engineering, 2007

2006

A logic for information flow in object-oriented programs.

[BibT_eX]

[DOI]

Sruthi Bandhakavi

Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2006

Automata-Based Confidentiality Monitoring.

[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

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

Information Flow Analysis in Logical Form.

[BibT_eX]

[DOI]

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

History-Based Access Control and Secure Information Flow.

[BibT_eX]

[DOI]

Proceedings of the Construction and Analysis of Safe, 2004

2003

Modular Control-Flow Analysis with Rank 2 Intersection Types.

[BibT_eX]

[DOI]

Thomas P. Jensen

Math. Struct. Comput. Sci., 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

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

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

Design and Correctness of Program Transformations Based on Control-Flow Analysis.

[BibT_eX]

[DOI]

Nevin Heintze

Jon G. Riecke

Proceedings of the Theoretical Aspects of Computer Software, 4th International Symposium, 2001

1999

A Core Calculus of Dependency.

[BibT_eX]

[DOI]

Proceedings of the POPL '99, 1999

Region Analysis and the Polymorphic Lambda Calculus.

[BibT_eX]

[DOI]

Nevin Heintze

Jon G. Riecke

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998

Stackability in the Simply-Typed Call-by-Value lambda Calculus.

[BibT_eX]

[DOI]

David A. Schmidt

Sci. Comput. Program., 1998

1997

A Modular, Polyvariant, and Type-Based Closure Analysis.

[BibT_eX]

[DOI]

Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP '97), 1997

1993

A Categorical Interpretation of Landin's Correspondence Principle.

[BibT_eX]

[DOI]