Alasdair Armstrong

28 papers A* 1A 3B 5C 4Journal 13Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures.
Proc. ACM Program. Lang.
Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, Peter Sewell
2025 J jnl
Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor.
CoRR
Louis-Emile Ploix, Alasdair Armstrong, Tom Melham, Ray Lin, Haolong Wang, Anastasia Courtney
2025 A* conf
Precise exceptions in relaxed architectures.
ISCA
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2024 J jnl
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version).
Formal Methods Syst. Des.
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2024 J jnl
Relaxed exception semantics for Arm-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Ohad Kammar, Jean Pichon-Pharabod, Peter Sewell
2022 J jnl
Relaxed virtual memory in Armv8-A (extended version).
CoRR
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2022 A conf
Relaxed virtual memory in Armv8-A.
ESOP
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
2022 A conf
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture.
ESOP
Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell
2021 — conf
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models.
CAV (1)
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
2020 A conf
ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures.
ESOP
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell
2019 J jnl
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS.
Proc. ACM Program. Lang.
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, Peter Sewell
2018 B conf
On abstraction and compositionality for weak-memory linearisability.
VMCAI
Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong
2017 C conf
Modularising Opacity Verification for Hybrid Transactional Memory.
FORTE
Alasdair Armstrong, Brijesh Dongol
2017 C conf
Proving Opacity via Linearizability: A Sound and Complete Method.
FORTE
Alasdair Armstrong, Brijesh Dongol, Simon Doherty
2016 J jnl
Building program construction and verification tools from algebraic principles.
Formal Aspects Comput.
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
2016 J jnl
Reducing Opacity to Linearizability: A Sound and Complete Method.
CoRR
Alasdair Armstrong, Brijesh Dongol, Simon Doherty
2015 — —
Formal analysis of concurrent programs.
Alasdair Armstrong
2014 B conf
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools.
FM
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
2014 C conf
Algebras for Program Correctness in Isabelle/HOL.
RAMiCS
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
2014 J jnl
Kleene Algebra with Tests and Demonic Refinement Algebras.
Arch. Formal Proofs
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
2014 B conf
Lightweight Program Construction and Verification Tools in Isabelle/HOL.
SEFM
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
2014 J jnl
Programming and automating mathematics in the Tarski-Kleene hierarchy.
J. Log. Algebraic Methods Program.
Alasdair Armstrong, Georg Struth, Tjark Weber
2013 J jnl
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools.
CoRR
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
2013 J jnl
Kleene Algebra.
Arch. Formal Proofs
Alasdair Armstrong, Georg Struth, Tjark Weber
2013 B conf
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL.
ITP
Alasdair Armstrong, Georg Struth, Tjark Weber
2012 C conf
Automated Reasoning in Higher-Order Regular Algebra.
RAMiCS
Alasdair Armstrong, Georg Struth
2012 B conf
Dependently Typed Programming Based on Automated Theorem Proving.
MPC
Alasdair Armstrong, Simon Foster, Georg Struth
2011 J jnl
Dependently Typed Programming based on Automated Theorem Proving
CoRR
Alasdair Armstrong, Simon Foster, Georg Struth