2 papers
cs.AR2025
Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor
Louis-Emile Ploix, Alasdair Armstrong, Tom Melham +3
The CHERI architecture equips conventional RISC ISAs with significant architectural extensions that provide a hardware-enforced mechanism for memory protection and software compart…
cs.AR2024
Relaxed exception semantics for Arm-A (extended version)
Ben Simner, Alasdair Armstrong, Thomas Bauereiss +4
To manage exceptions, software relies on a key architectural guarantee, precision: that exceptions appear to execute between instructions. However, this definition, dating back ove…