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
Dalvandi M
(2019)
Towards deductive verification of C11 programs with Event-B and ProB
Dalvandi S
(2021)
Verifying C11-style weak memory libraries
Dalvandi S
(2022)
Implementing and verifying release-acquire transactional memory in C11
in Proceedings of the ACM on Programming Languages
Dalvandi S
(2021)
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
in Journal of Automated Reasoning
Dalvandi S
(2021)
Verifying C11-style weak memory libraries
Derrick J
(2021)
Verifying correctness of persistent concurrent data structures: a sound and complete method
in Formal Aspects of Computing
| 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 | 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. 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... |
| 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... |
| 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 | 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... |
| 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... |
| 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... |