Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)

Autor: Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell

Publikováno v: Armstrong, A, Campbell, B, Simner, B, Pulte, C & Sewell, P 2023, ' Isla: Integrating full-scale ISA semantics and axiomatic concurrency models (extended version) ', Formal Methods in System Design . https://doi.org/10.1007/s10703-023-00409-y

Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::69b2e52e31ae585251c82019a5b3e9b7
https://doi.org/10.1007/s10703-023-00409-y

Verified security for the Morello capability-enhanced prototype Arm architecture

Autor: Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell

Publikováno v: Programming Languages and Systems ISBN: 9783030993351
Bauereiss, T, Campbell, B, Sewell, T, Armstrong, A, Esswood, L, Stark, I, Barnes, G, Watson, R N M & Sewell, P 2022, Verified Security for the Morello Capability-enhanced Prototype Arm Architecture . in I Sergey (ed.), Programming Languages and Systems-31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings . Lecture Notes in Computer Science, vol. 13240, pp. 174-203, 31st European Symposium on Programming, Munich, Bavaria, Germany, 2/04/22 . https://doi.org/10.1007/978-3-030-99336-8_7
Lecture Notes in Computer Science
Lecture Notes in Computer Science-Programming Languages and Systems

Memory safety bugs continue to be a major source of security vulnerabilities in our critical infrastructure. The CHERI project has proposed extending conventional architectures with hardware-supported capabilities to enable fine-grained memory protec

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e33b27cf5d89ec8d861535ebdebf90f8

Building program construction and verification tools from algebraic principles

Autor: Victor B. F. Gomes, Georg Struth, Alasdair Armstrong

Publikováno v: Formal Aspects of Computing. 28:265-293

We present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with tes

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::dcdb98f0c9ded5cadcac43ce04acfb43
https://doi.org/10.1007/s00165-015-0343-1

Proving Opacity via Linearizability: A Sound and Complete Method

Autor: Brijesh Dongol, Alasdair Armstrong, Simon Doherty

Publikováno v: Formal Techniques for Distributed Objects, Components, and Systems ISBN: 9783319602240
FORTE

Transactional memory (TM) is a mechanism that manages thread synchronisation on behalf of a programmer so that blocks of code execute with the illusion of atomicity. The main safety criterion for transactional memory is opacity, which defines conditi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::3ff03fcbdc064ad57556b5e62903933b
https://doi.org/10.1007/978-3-319-60225-7_4

Algebras for Program Correctness in Isabelle/HOL

Autor: Georg Struth, Victor B. F. Gomes, Alasdair Armstrong

Publikováno v: Relational and Algebraic Methods in Computer Science ISBN: 9783319062501
RAMICS

We present a reference formalisation of Kleene algebra and demonic refinement algebra with tests in Isabelle/HOL. It provides three different formalisations of tests. Our structured comprehensive libraries for these algebras extend an existing Kleene

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::8ad1aa81582ab86be754f03c951d282a
https://doi.org/10.1007/978-3-319-06251-8_4