Writing formal specifications at ARM

Talk by Jade Alglave, Arm and University College London


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.