Arm is an instruction set architecture.

Formal ISA specifications for Arm include

• Specification from Arm written in ASL.

• Specification from Cambridge University mechanically translated to Sail from the ASL specification.

• L3 specification from Cambridge University.

Notes related to Arm architecture

Arm Architecture Specification Language (ASL), Capstone disassembler, Instruction set architecture, L3 specification language, Remill binary lifting library, Sail ISA specification language

Papers related to Arm architecture

• Detailed models of instruction set architectures: From pseudocode to formal semantics [armstrong:arw:2018]
• ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS [armstrong:popl19:2019]
• The state of Sail [armstrong:spisa:2019]
• A high assurance virtualization platform for ARMv8 [baumann:eucnc:2016]
• Advanced SIMD: Extending the reach of contemporary SIMD architectures [boettcher:date:2014]
• Machine code verification of a tiny ARM hypervisor [dam:ted:2013]
• Machine code verification of a tiny ARM hypervisor [dam:trusted:2013]
• Modelling the ARMv8 architecture, operationally: concurrency and ISA [flur:popl:2016]
• Mixed-size concurrency: ARM, POWER, C/C++11, and SC [flur:popl:2017]
• A HOL specification of the ARM instruction set architecture [fox:cambridge:2001]
• A trustworthy monadic formalization of the ARMv7 instruction set architecture [fox:itp:2010]
• Directions in ISA specification [fox:itp:2012]
• Improved tool support for machine-code decompilation in HOL4 [fox:itps:2015]
• Formal specification and verification of ARM6 [fox:tphols:2003]
• Formal verification of the ARM6 micro-architecture [fox:ucam:2002]
• GeST: An automatic framework for generating CPU stress-tests [hadjilambrou:ispass:2019]
• Examiner: Automatically locating inconsistent instructions between real devices and CPU emulators for Arm [jiang:arxiv:2021]
• Towards verified faithful simulation [joloboff:dsetta:2015]
• Machine assisted proof of ARMv7 instruction level isolation properties [khakpour:cpp:2013]
• Pydgin: generating fast instruction set simulators from simple architecture descriptions with meta-tracing JIT compilers [lockhart:ispass:2015]
• Verified LISP Implementations on ARM, x86 and PowerPC [myreen:tphols:2009]
• Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8 [pulte:popl:2017]
• 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]
• Who guards the guards? Formal validation of the ARM v8-M architecture specification [reid:oopsla:2017]
• Defining interfaces between hardware and software: Quality and performance [reid:phd:2019]
• Automatic derivation of platform noninterference properties [schwarz:sefm:2016]
• ARM Architecture Reference Manual (ARMv5 edition) [seal:book:2000]
• Translation validation for a verified OS kernel [sewell:pldi:2013]
• Certification of an instruction set simulator [shi:phd:2013]
• ARMv8-A system semantics: Instruction fetch in relaxed architectures [simner:pls:2020]
• The ARM scalable vector extension [stephens:micro:2017]
• Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]
• A new verified compiler backend for CakeML [tan:icfp:2016]
• Formal verification of a multiprocessor hypervisor on Arm relaxed memory hardware [tao:sosp:2021]
• Raising binaries to LLVM IR with MCTOLL (WIP paper) [yadavalli:lctes:2019]