Skip to main content

OxWoCS Seminar Series: Writing Formal Specifications in Arm

Professor Jade Alglave ( UCL and Arm )

We're delighted to invite Professor Jade Alglave, UCL and Arm, on Thursday 31st October at 3:00PM in the Bill Roscoe Lecture Theatre (LT B).

Title: Writing Formal Specifications in Arm

Abstract:

In this talk I will give an overview of the progress made by my team, the Arm Architecture Formal Team, on writing formal specifications. Initially focussed on the memory model, we have recently expanded our work to writing a definition for ASL, the Architecture Specification Language used at Arm to describe how instructions behave. I will talk about both those areas and present the work to date.

Please use the following link to register your interest so that we can provide sufficient refreshments: Register here

Speaker bio

Dr Jade Alglave FREng Distinguished Engineer, Arm Ltd; and Professor of Computer Science, University College London (UCL)

Professor Jade Alglave, Distinguished Engineer at Arm and Professor at UCL, developed a novel mathematical method of specifying computer memory models, an associated language (cat) and software tools (herd, diy) for writing and experimenting with the models, in tandem with Luc Maranget (INRIA, France). She has been recognised for significant industrial impact through memory models for IBM, NVidia, Heterogenous System Architecture (HSA), Arm and Linux. She navigated the complex world of hardware, low-level software, mathematical modelling techniques, tools, and various scientific and business communities to deliver an innovative series of tools and techniques. Professor Alglave won the Royal Society Brian Mercer Award for Innovation in 2014, the Royal Academy of Engineering Silver Medal in 2018 and the British Computer Society Roger Needham Award in 2020.

 

 

Share this: