Speaker
Jade Alglave
University College London, UK
Bio
Jade is a Professor of Computer Science at University College London, a Fellow of the Royal Academy of Engineering, and a Fellow at Arm, where she leads the Arm Architecture Formal Team.
The Arm Architecture Formal Team looks after the Arm Concurrency Model, a machine-readable, executable and formal artefact [0] which can be interpreted by the herd tool [1, 2] to determine which values a load instruction may read in a concurrent program written in Arm assembly. This artefact guides the generation of the English prose that appears in the Arm Architecture Reference Manual. The Arm Architecture Formal Team also looks after the Architecture Specification Language, a domain-specific language used at Arm to write the semantics of the ISA. This language itself has a formal semantics and type system [3, 4], out of which the specification can be generated [5], and the team develops and maintains the Arm reference interpreter and type-checker for the language [6, 7].
Beyond formal methods, the team also contributes to the design and developement of other tools, for example to enhance the searchability and accessibility of Arm specifications, such as The Architecture Speaks chatbot [7]. The team’s formal expertise comes into play when devising strategies to check the accuracy of The Architecture Speaks chatbot’s answers.