Specifying the de-facto OS of a production SoC
Ben Fiedler, R. Meier, Jasmin Schult, Daniel Schwyn, Timothy Roscoe · 2023
Verification of any operating system is inevitably relative to a model of the underlying hardware. Within the context of kernel verification, the underlying hardware model usually comprises of architectural correctness of the executing cores, but pays little attention to devices underneath barring the assumption that they are "trusted".