Verifiably Correct Transactional Memory
Lead Research Organisation:
University of Surrey
Department Name: Computing Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Organisations
Publications
Wright D
(2023)
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies
in Formal Aspects of Computing
Semenyuk M
(2023)
Ownership-Based Owicki-Gries Reasoning
Lam T
(2020)
A blockchain-enabled e-learning platform
in Interactive Learning Environments
Kulik T
(2021)
A Survey of Practical Formal Methods for Security
Kulik T
(2022)
A Survey of Practical Formal Methods for Security
in Formal Aspects of Computing
Dongol B.
(2021)
Convolution algebras: Relational convolution, generalised modalities and incidence algebras
in Logical Methods in Computer Science
Dongol B.
(2019)
Preface
in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Dongol B.
(2022)
Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement
in Leibniz International Proceedings in Informatics, LIPIcs
Dongol B.
(2020)
Preface
in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Dongol B
(2021)
Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras
in Logical Methods in Computer Science
Dongol B
(2019)
Modular transactions
Dongol B
(2017)
Transactions in relaxed memory architectures
in Proceedings of the ACM on Programming Languages
Doherty S
(2019)
Verifying C11 programs operationally
Doherty S
(2022)
Unifying Operational Weak Memory Verification: An Axiomatic Approach
in ACM Transactions on Computational Logic
Derrick J.
(2021)
Brief announcement: On strong observational refinement and forward simulation
in Leibniz International Proceedings in Informatics, LIPIcs
Description | We have developed a series of new logics to reason about concurrent programs over advanced memory models. This, includes a programming language (C/C++) and a non-volatile memory (persistent x86) developed by Intel. We have used these logics to verify complex concurrent programs. This work will ultimately enable development of more trustworthy programs. We have tackled both concurrent objects (e.g., as implemented in Facebook's Folly library) and transactional memory libraries. |
Exploitation Route | Our logic can be used as a basis to prove other (more complex) concurrent programs. Our modular technique allows program composition and library development. We have tackled both concurrent objects (e.g., as implemented in Facebook's Folly library) and transactional memory libraries. |
Sectors | Digital/Communication/Information Technologies (including Software),Education |
Description | Amazon Gift |
Amount | £100,000 (GBP) |
Organisation | Amazon.com |
Sector | Private |
Country | United States |
Start | 10/2020 |
Description | Design and verification of correct, efficient and secure concurrent systems |
Amount | $460,000 (AUD) |
Funding ID | DP190102142 |
Organisation | Australian Research Council |
Sector | Public |
Country | Australia |
Start | 01/2019 |
End | 12/2021 |
Description | FACT: Faithful Composition of Trust |
Amount | £204,000 (GBP) |
Organisation | National Cyber Security Centre |
Sector | Public |
Country | United Kingdom |
Start | 10/2019 |
End | 03/2021 |
Description | Persistent Safety and Security |
Amount | £78,000 (GBP) |
Organisation | The Research Institute on Verified Trustworthy Software Systems |
Sector | Academic/University |
Country | United Kingdom |
Start | 10/2019 |
End | 03/2023 |
Description | Transactional Memory Security |
Amount | £31,063 (GBP) |
Organisation | National Cyber Security Centre |
Sector | Public |
Country | United Kingdom |
Start | 01/2021 |
End | 03/2021 |
Title | Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" |
Description | Isabelle/HOL files for "Ownership-Based Owicki-Gries Reasoning" accepted to SAC 2023. The theories have been tested on Isabelle 2022. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_HOL_files_for_Ownership-Based_Owicki-Gries_Reasoning... |
Title | Tamarin Models for "Verifying List Swarm Attestation Protocols" |
Description | Tamarin models and proofs of SIMPLE+ and its variations for the paper "Verifying List Swarm Attestation Protocols" to appear in WiSEC 2023. https://doi.org/10.1145/3558482.3581778 The proofs have been tested with Tamarin 1.6.1. |
Type Of Technology | Software |
Year Produced | 2023 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Tamarin_Models_for_Verifying_List_Swarm_Attestation_Protocols... |
Description | FDR models for the SEFM 2021 paper "Checking Opacity and Durable Opacity with FDR" |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/FDR_models_for_Checking_Opacity_and_Durable_Opacity_with_FDR_... |
Description | Isabelle files for "Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL".The proofs require Isabelle/HOL 2020. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_Files_for_Integrating_Owicki-Gries_for_C11-Style_Mem... |
Description | Isabelle files for "Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL".The proofs require Isabelle/HOL 2020. |
Type Of Technology | Software |
Year Produced | 2021 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_Files_for_Integrating_Owicki-Gries_for_C11-Style_Mem... |
Description | Isabelle/HOL files for "View-Based Owicki-Gries Reasoning for Persistent x86-TSO" published in ESOP 2022. |
Type Of Technology | Software |
Year Produced | 2022 |
Open Source License? | Yes |
URL | https://figshare.com/articles/software/Isabelle_files_for_View-Based_Owicki-Gries_Reasoning_for_Pers... |