Alasdair Armstrong

Publication Activity (10 Years)

Years Active: 2011-2022
Publications (10 Years): 11

Top Venues

CoRR

ESOP

FORTE

Arch. Formal Proofs

University of Sheffield, UK (PHD)

Education History

University of Sheffield, UK

PHD

Publications

Thomas Bauereiss, Brian Campbell, Thomas Sewell, Alasdair Armstrong, Lawrence Esswood, Ian Stark, Graeme Barnes, Robert N. M. Watson, Peter Sewell
Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. ESOP (2022)
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
Relaxed virtual memory in Armv8-A. ESOP (2022)
Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell
Relaxed virtual memory in Armv8-A (extended version). CoRR (2022)
Alasdair Armstrong, Brian Campbell, Ben Simner, Christopher Pulte, Peter Sewell
Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. CAV (1) (2021)
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell
ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures. ESOP (2020)
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
ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. Proc. ACM Program. Lang. 3 (POPL) (2019)
Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong
On abstraction and compositionality for weak-memory linearisability. VMCAI (2018)
Alasdair Armstrong, Brijesh Dongol, Simon Doherty
Proving Opacity via Linearizability: A Sound and Complete Method. FORTE (2017)
Alasdair Armstrong, Brijesh Dongol
Modularising Opacity Verification for Hybrid Transactional Memory. FORTE (2017)
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Building program construction and verification tools from algebraic principles. Formal Aspects Comput. 28 (2) (2016)
Alasdair Armstrong, Brijesh Dongol, Simon Doherty
Reducing Opacity to Linearizability: A Sound and Complete Method. CoRR (2016)
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools. FM (2014)
Alasdair Armstrong, Georg Struth, Tjark Weber
Programming and automating mathematics in the Tarski-Kleene hierarchy. J. Log. Algebraic Methods Program. 83 (2) (2014)
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Kleene Algebra with Tests and Demonic Refinement Algebras. Arch. Formal Proofs 2014 (2014)
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Lightweight Program Construction and Verification Tools in Isabelle/HOL. SEFM (2014)
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Algebras for Program Correctness in Isabelle/HOL. RAMiCS (2014)
Alasdair Armstrong, Georg Struth, Tjark Weber
Kleene Algebra. Arch. Formal Proofs 2013 (2013)
Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools. CoRR (2013)
Alasdair Armstrong, Georg Struth, Tjark Weber
Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. ITP (2013)
Alasdair Armstrong, Georg Struth
Automated Reasoning in Higher-Order Regular Algebra. RAMiCS (2012)
Alasdair Armstrong, Simon Foster, Georg Struth
Dependently Typed Programming Based on Automated Theorem Proving. MPC (2012)
Alasdair Armstrong, Simon Foster, Georg Struth
Dependently Typed Programming based on Automated Theorem Proving CoRR (2011)

Alasdair Armstrong.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Alasdair Armstrong