Alasdair Armstrong

According to our database, Alasdair Armstrong authored at least 22 papers between 2012 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

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

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

Formal Methods Syst. Des., October, 2024

2022

Relaxed virtual memory in Armv8-A (extended version).

Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell

CoRR, 2022

Relaxed virtual memory in Armv8-A.

Ben Simner, Alasdair Armstrong, Jean Pichon-Pharabod, Christopher Pulte, Richard Grisenthwaite, Peter Sewell

Proceedings of the Programming Languages and Systems, 2022

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture.

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

Proceedings of the Programming Languages and Systems, 2022

2021

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models.

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

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures.

Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell

Proceedings of the Programming Languages and Systems, 2020

2019

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS.

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

Proc. ACM Program. Lang., 2019

2018

On abstraction and compositionality for weak-memory linearisability.

Brijesh Dongol, Radha Jagadeesan, James Riely, Alasdair Armstrong

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

2017

Proving Opacity via Linearizability: A Sound and Complete Method.

Alasdair Armstrong, Brijesh Dongol, Simon Doherty

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

Modularising Opacity Verification for Hybrid Transactional Memory.

Alasdair Armstrong, Brijesh Dongol

Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

2016

Building program construction and verification tools from algebraic principles.

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

Formal Aspects Comput., 2016

Reducing Opacity to Linearizability: A Sound and Complete Method.

Alasdair Armstrong, Brijesh Dongol, Simon Doherty

CoRR, 2016

2015

Formal analysis of concurrent programs.

Alasdair Armstrong

PhD thesis, 2015

2014

Programming and automating mathematics in the Tarski-Kleene hierarchy.

Alasdair Armstrong, Georg Struth, Tjark Weber

J. Log. Algebraic Methods Program., 2014

Kleene Algebra with Tests and Demonic Refinement Algebras.

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

Arch. Formal Proofs, 2014

Lightweight Program Construction and Verification Tools in Isabelle/HOL.

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

Proceedings of the Software Engineering and Formal Methods - 12th International Conference, 2014

Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools.

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

Proceedings of the FM 2014: Formal Methods, 2014

Algebras for Program Correctness in Isabelle/HOL.

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

Proceedings of the Relational and Algebraic Methods in Computer Science, 2014

2013

Kleene Algebra.

Alasdair Armstrong, Georg Struth, Tjark Weber

Arch. Formal Proofs, 2013

Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL.

Alasdair Armstrong, Georg Struth, Tjark Weber

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Dependently Typed Programming Based on Automated Theorem Proving.

Alasdair Armstrong, Simon Foster, Georg Struth

Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Automated Reasoning in Higher-Order Regular Algebra.

Alasdair Armstrong, Georg Struth

Proceedings of the Relational and Algebraic Methods in Computer Science, 2012