Brijesh Dongol

Inroads, December, 2024

Operationally proving memory access violations in Isabelle/HOL.

[BibT_eX]

[DOI]

Sharar Ahmadi

Matt Griffin

Sci. Comput. Program., 2024

On the Design and Security of Collective Remote Attestation Protocols.

[BibT_eX]

[DOI]

CoRR, 2024

Secret-Directed Unwinding.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2024

What Cannot Be Implemented on Weak Memory?

[BibT_eX]

[DOI]

Proceedings of the 38th International Symposium on Distributed Computing, 2024

A Fully Verified Persistency Library.

[BibT_eX]

[DOI]

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

Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM.

[BibT_eX]

[DOI]

Proceedings of the 2024 USENIX Annual Technical Conference, 2024

Unifying Weak Memory Verification Using Potentials.

[BibT_eX]

[DOI]

Lara Bargmann

Proceedings of the Formal Methods - 26th International Symposium, 2024

Artifact Report: Intel PMDK Transactions: Specification, Validation and Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2024

Intel PMDK Transactions: Specification, Validation and Concurrency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2024

Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities.

[BibT_eX]

[DOI]

Proceedings of the 37th IEEE Computer Security Foundations Symposium, 2024

2023

Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies.

[BibT_eX]

[DOI]

Formal Aspects Comput., June, 2023

Intel PMDK Transactions: Specification, Validation and Concurrency (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2023

Rely-Guarantee Reasoning for Causally Consistent Shared Memory (Extended Version).

[BibT_eX]

[DOI]

Ori Lahav

CoRR, 2023

Verifying List Swarm Attestation Protocols.

[BibT_eX]

[DOI]

Proceedings of the 16th ACM Conference on Security and Privacy in Wireless and Mobile Networks, 2023

Verifying Read-Copy Update Under RC11.

[BibT_eX]

[DOI]

Mikhail Semenyuk

Mark Batty

Proceedings of the Software Engineering and Formal Methods - 21st International Conference, 2023

Ownership-Based Owicki-Gries Reasoning.

[BibT_eX]

[DOI]

Mikhail Semenyuk

Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing, 2023

Reasoning About Promises in Weak Memory Models with Event Structures.

[BibT_eX]

[DOI]

Lara Bargmann

Proceedings of the Formal Methods - 25th International Symposium, 2023

Rely-Guarantee Reasoning for Causally Consistent Shared Memory.

[BibT_eX]

[DOI]

Ori Lahav

Proceedings of the Computer Aided Verification - 35th International Conference, 2023

2022

Unifying Operational Weak Memory Verification: An Axiomatic Approach.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2022

Implementing and verifying release-acquire transactional memory in C11.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2022

Modularising Verification Of Durable Opacity.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2022

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.

[BibT_eX]

[DOI]

J. Autom. Reason., 2022

A blockchain-enabled e-learning platform.

[BibT_eX]

[DOI]

Tsz Yiu Lam

Peter W. V. Tran-Jørgensen

Interact. Learn. Environ., 2022

A Survey of Practical Formal Methods for Security.

[BibT_eX]

[DOI]

Jim Woodcock

Formal Aspects Comput., 2022

Introduction to the Special Section on iFM 2020.

[BibT_eX]

[DOI]

Elena Troubitsyna

Formal Aspects Comput., 2022

Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version).

[BibT_eX]

[DOI]

Lara Bargmann

CoRR, 2022

Implementing and Verifying Release-Acquire Transactional Memory (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2022

View-Based Owicki-Gries Reasoning for Persistent x86-TSO (Extended Version).

[BibT_eX]

[DOI]

CoRR, 2022

Proving Memory Access Violations in Isabelle/HOL.

[BibT_eX]

[DOI]

Sharar Ahmadi

Matt Griffin

Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, 2022

View-Based Owicki-Gries Reasoning for Persistent x86-TSO.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2022

Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement.

[BibT_eX]

[DOI]

Gerhard Schellhorn

Proceedings of the 33rd International Conference on Concurrency Theory, 2022

2021

Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2021

Verifying correctness of persistent concurrent data structures: a sound and complete method.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2021

Verifying C11-Style Weak Memory Libraries via Refinement.

[BibT_eX]

[DOI]

CoRR, 2021

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version).

[BibT_eX]

[DOI]

Daniel Wright

Mark Batty

CoRR, 2021

On Strong Observational Refinement and Forward Simulation.

[BibT_eX]

[DOI]

CoRR, 2021

Brief Announcement: On Strong Observational Refinement and Forward Simulation.

[BibT_eX]

[DOI]

Proceedings of the 35th International Symposium on Distributed Computing, 2021

Checking Opacity and Durable Opacity with FDR.

[BibT_eX]

[DOI]

Jay Le-Papin

Proceedings of the Software Engineering and Formal Methods - 19th International Conference, 2021

Verifying C11-style weak memory libraries.

[BibT_eX]

[DOI]

Proceedings of the PPoPP '21: 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2021

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies.

[BibT_eX]

[DOI]

Daniel Wright

Mark Batty

Proceedings of the Formal Methods - 24th International Symposium, 2021

Verifying Secure Speculation in Isabelle/HOL.

[BibT_eX]

[DOI]

Matt Griffin

Proceedings of the Formal Methods - 24th International Symposium, 2021

2020

Owicki-Gries Reasoning for C11 RAR (Artifact).

[BibT_eX]

[DOI]

Dagstuhl Artifacts Ser., 2020

Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL.

[BibT_eX]

[DOI]

Simon Doherty

CoRR, 2020

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2020

Owicki-Gries Reasoning for C11 RAR.

[BibT_eX]

[DOI]

Proceedings of the 34th European Conference on Object-Oriented Programming, 2020

2019

Modular transactions: bounding mixed races in space and time.

[BibT_eX]

[DOI]

Radha Jagadeesan

James Riely

Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2019

Verifying C11 programs operationally.

[BibT_eX]

[DOI]

Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2019

Cylindric Kleene Lattices for Program Construction.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

Verifying Correctness of Persistent Concurrent Data Structures.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs.

[BibT_eX]

[DOI]

Keith Clark

Peter Robinson

Proceedings of the Formal Methods. FM 2019 International Workshops, 2019

Towards deductive verification of C11 programs with Event-B and ProB.

[BibT_eX]

[DOI]

Mohammadsadegh Dalvandi

Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, 2019

2018

Transactions in relaxed memory architectures.

[BibT_eX]

[DOI]

Radha Jagadeesan

James Riely

Proc. ACM Program. Lang., 2018

Mechanized proofs of opacity: a comparison of two techniques.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2018

Causal Linearizability: Compositionality for Partially Ordered Executions.

[BibT_eX]

[DOI]

CoRR, 2018

Brief Announcement: Generalising Concurrent Correctness to Weak Memory.

[BibT_eX]

[DOI]

Proceedings of the 32nd International Symposium on Distributed Computing, 2018

On abstraction and compositionality for weak-memory linearisability.

[BibT_eX]

[DOI]

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

Making Linearizability Compositional for Partially Ordered Executions.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 14th International Conference, 2018

2017

Decidability and complexity for quiescent consistency and its variations.

[BibT_eX]

[DOI]

Robert M. Hierons

Inf. Comput., 2017

Relational Convolution, Generalised Modalities and Incidence Algebras.

[BibT_eX]

[DOI]

CoRR, 2017

Partial Semigroups and Convolution Algebras.

[BibT_eX]

[DOI]

Arch. Formal Proofs, 2017

Proving Opacity via Linearizability: A Sound and Complete Method.

[BibT_eX]

[DOI]

Alasdair Armstrong

Simon Doherty

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

Modularising Opacity Verification for Hybrid Transactional Memory.

[BibT_eX]

[DOI]

Alasdair Armstrong

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

A Proof Method for Linearizability on TSO Architectures.

[BibT_eX]

[DOI]

Proceedings of the Provably Correct Systems, 2017

2016

Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2016

Reducing Opacity to Linearizability: A Sound and Complete Method.

[BibT_eX]

[DOI]

Alasdair Armstrong

Simon Doherty

CoRR, 2016

Proving Opacity of a Pessimistic STM.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Principles of Distributed Systems, 2016

Decidability and Complexity for Quiescent Consistency.

[BibT_eX]

[DOI]

Robert M. Hierons

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Contextual Trace Refinement for Concurrent Objects: Safety and Progress.

[BibT_eX]

[DOI]

Lindsay Groves

Proceedings of the Formal Methods and Software Engineering, 2016

An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Safety-Critical Systems, 2016

2015

Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2015

Verifying Linearisability: A Comparative Survey.

[BibT_eX]

[DOI]

ACM Comput. Surv., 2015

Towards linking correctness conditions for concurrent objects and contextual trace refinement.

[BibT_eX]

[DOI]

Lindsay Groves

Proceedings of the Proceedings 17th International Workshop on Refinement, 2015

A Program Construction and Verification Tool for Separation Logic.

[BibT_eX]

[DOI]

Victor B. F. Gomes

Proceedings of the Mathematics of Program Construction - 12th International Conference, 2015

Verifying Opacity of a Transactional Mutex Lock.

[BibT_eX]

[DOI]

Proceedings of the FM 2015: Formal Methods, 2015

Defining Correctness Conditions for Concurrent Objects in Multicore Architectures.

[BibT_eX]

[DOI]

Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014

Deriving real-time action systems with multiple time bands using algebraic reasoning.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2014

Reasoning about goal-directed real-time teleo-reactive programs.

[BibT_eX]

[DOI]

Peter J. Robinson

Formal Aspects Comput., 2014

Convolution, Separation and Concurrency.

[BibT_eX]

[DOI]

CoRR, 2014

Principles for Verification Tools: Separation Logic.

[BibT_eX]

[DOI]

Victor B. F. Gomes

CoRR, 2014

Verifying linearizability: A comparative survey.

[BibT_eX]

[DOI]

CoRR, 2014

Verifying Linearizability on TSO Architectures.

[BibT_eX]

[DOI]

Graeme Smith

Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Reasoning Algebraically About Refinement on TSO Architectures.

[BibT_eX]

[DOI]

Graeme Smith

Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures.

[BibT_eX]

[DOI]

Proceedings of the Hardware and Software: Verification and Testing, 2014

Quiescent Consistency: Defining and Verifying Relaxed Linearizability.

[BibT_eX]

[DOI]

Proceedings of the FM 2014: Formal Methods, 2014

Admit Your Weakness: Verifying Correctness on TSO Architectures.

[BibT_eX]

[DOI]

Graeme Smith

Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

2013

Deriving real-time action systems in a sampling logic.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2013

Simplifying proofs of linearisability using layers of abstraction.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013

Data refinement for true concurrency

[BibT_eX]

[DOI]

Proceedings of the Proceedings 16th International Refinement Workshop, 2013

Comparing Degrees of Non-Determinism in Expression Evaluation.

[BibT_eX]

[DOI]

Comput. J., 2013

A High-Level Semantics for Program Execution under Total Store Order Memory.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

2012

Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Proving linearisability via coarse-grained abstraction

[BibT_eX]

[DOI]

CoRR, 2012

Deriving Real-Time Action Systems Controllers from Multiscale System Specifications.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Rely/Guarantee Reasoning for Teleo-reactive Programs over Multiple Time Bands.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods - 9th International Conference, 2012

Towards an Algebra for Real-Time Programs.

[BibT_eX]

[DOI]

Proceedings of the Relational and Algebraic Methods in Computer Science, 2012

2011

Approximating Idealised Real-Time Specifications Using Time Bands.

[BibT_eX]

[DOI]

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2011

2010

Compositional Action System Derivation Using Enforced Properties.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

2009

Progress-based verification and derivation of concurrent programs

[BibT_eX]

[DOI]

PhD thesis, 2009

A general technique for proving lock-freedom.

[BibT_eX]

[DOI]

Robert Colvin

Sci. Comput. Program., 2009

Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation.

[BibT_eX]

[DOI]

Proceedings of the 20th Australian Software Engineering Conference (ASWEC 2009), 2009

2008

Streamlining progress-based derivations of concurrent programs.

[BibT_eX]

[DOI]

Arjan J. Mooij

Formal Aspects Comput., 2008

2007

Verifying Lock-Freedom Using Well-Founded Orders.

[BibT_eX]

[DOI]

Robert Colvin

Proceedings of the Theoretical Aspects of Computing, 2007

2006

Extending the theory of Owicki and Gries with a logic of progress.

[BibT_eX]

[DOI]

Doug Goldson

Log. Methods Comput. Sci., 2006

Progress in Deriving Concurrent Programs: Emphasizing the Role of Stable Guards.

[BibT_eX]

[DOI]

Arjan J. Mooij

Proceedings of the Mathematics of Program Construction, 8th International Conference, 2006

Formalising Progress Properties of Non-blocking Programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2006

Derivation of Java Monitors.

[BibT_eX]

[DOI]

Proceedings of the 17th Australian Software Engineering Conference (ASWEC 2006), 2006

2005

Concurrent Program Design in the Extended Theory of Owicki and Gries.

[BibT_eX]

[DOI]

Doug Goldson