Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT)
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.
Publications
Griffin M
(2024)
A Binary Analysis Platform in Isabelle/HOL
VafeiadiĀ Bila E
(2024)
A verified durable transactional mutex lock for persistent x86-TSO
in Formal Methods in System Design
Egorov S.
(2024)
Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM
in Proceedings of the 2024 USENIX Annual Technical Conference, ATC 2024
Wright D
(2023)
Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies
in Formal Aspects of Computing
Dongol B
(2024)
On Formal Methods Thinking in Computer Science Education
in Formal Aspects of Computing
Ahmadi S
(2024)
Operationally proving memory access violations in Isabelle/HOL
in Science of Computer Programming
| Description | ARM |
| Organisation | Arm Limited |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Dongol together with Prof John Derrick and Dr Simon Doherty travelled to ARM (Cambridge) to discuss potential for collaborative work with ARM. Dongol gave a presentation (via a lunch-and-learn session), followed by a discussion about the most imminent problems for verification at ARM. |
| Collaborator Contribution | ARM have provided some feedback on our work and discussed the methods that would have most impact. |
| Impact | Dr Stephan Diestelhorst at ARM is an industrial collaborator on my new EPSRC grant (under review). |
| Start Year | 2016 |