2 citations · 7 across the 6 of their papers we have counts for
6 papers
Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor
Louis-Emile Ploix, Alasdair Armstrong, Tom Melham +3
The CHERI architecture equips conventional RISC ISAs with significant architectural extensions that provide a hardware-enforced mechanism for memory protection and software compart…
Relaxed exception semantics for Arm-A (extended version)
Ben Simner, Alasdair Armstrong, Thomas Bauereiss +4
To manage exceptions, software relies on a key architectural guarantee, precision: that exceptions appear to execute between instructions. However, this definition, dating back ove…
Relaxed virtual memory in Armv8-A (extended version)
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod +3
Virtual memory is an essential mechanism for enforcing security boundaries, but its relaxed-memory concurrency semantics has not previously been investigated in detail. The concurr…
Reducing Opacity to Linearizability: A Sound and Complete Method
Alasdair Armstrong, Brijesh Dongol, Simon Doherty
Transactional memory is a mechanism that manages thread synchronisation on behalf of a programmer so that blocks of code execute with an illusion of atomicity. The main safety crit…
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concre…
Dependently Typed Programming based on Automated Theorem Proving
Alasdair Armstrong, Simon Foster, Georg Struth
Mella is a minimalistic dependently typed programming language and interactive theorem prover implemented in Haskell. Its main purpose is to investigate the effective integration o…