Formal semantics for architectural description – Hadrien Renaud’s PhD project, co-supervised by Jade Alglave at UCL and Luc Maranget at INRIA
This PhD proposal aims to explore formal semantics for architectural description languages, such as the Arm Specification Language (ASL), and the domain-specific language called cat, which is used to describe the Arm memory model. Up until now, ASL did not even have a proper grammar, let alone any sort of formal semantics. We aim to explore semantics for ASL, and suitable abstractions thereof, in order to develop practical tools which would allow us to formally link the sequential descriptions of Arm instructions in ASL to their concurrency behaviour as described by the Arm memory model.
Hadrien has successfully passed his first year viva and published an article at the national conference “Journées Francophones des Langages Applicatifs”.
Congratulations Hadrien!
