The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
Machine-readable specifications for the Armv8 instruction set architecture have become publicly available as part of Arm’s release processes, providing an official and unambiguous source of truth for the semantics of Arm instructions. To date, compiler and machine code verification efforts have made use of unofficial theorem-proving-friendly specifications of Armv8, e.g. CakeML uses an L3-based specification. The validity of these verification efforts hinges upon their unofficial ISA specifications being valid with respect to the official Arm specification. Leveraging the Sail language ecosystem, we bridge this validation gap by formally verifying that an L3-based specification simulates the official Arm specification using the HOL4 interactive theorem prover. We exercise this simulation by proving a novel compiler correctness result for CakeML with respect to Arm’s official specification of the Armv8.6 A-class instruction set.
How it got here
How it got here
agent via openalex
Added
2026-10-26 12:35 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@article{kanabar2022taming,
title = {Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification},
author = {Hrutvik Kanabar and Anthony C. J. Fox and Magnus O. Myreen},
year = {2022},
journal = {DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)},
publisher = {Schloss Dagstuhl – Leibniz Center for Informatics},
doi = {10.4230/lipics.itp.2022.20},
}