Who guards the guards? Formal validation of the ARM v8-M architecture specification

Alastair D. Reid
[doi] [Google Scholar] [DBLP] [Citeseer]

PACMPL 1(OOPSLA)
Vancouver, BC, Canada
ACM
New York, NY, USA
Pages 88:1-88:24
22-27 October 2017
Note(s): ASL, Arm architecture, ISA specification, instruction set architecture, dependent type, natural language, requirements specification
Papers: reid:fmcad:2016, reid:cav:2016

Arm Architecture Specification Language (ASL)

  • Examiner: Automatically locating inconsistent instructions between real devices and CPU emulators for Arm [jiang:arxiv:2021]
  • End-to-end verification of ARM processors with ISA-formal [reid:cav:2016]
  • Trustworthy specifications of ARM v8-A and v8-M system level architecture [reid:fmcad:2016]
  • Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]