Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification

Shuanglong Kan, Sebastian Ertel

The Instruction Set Architecture (ISA) is the contract between compilers and processors; proving this contract formally demands cross-level connection to existing mechanized compil…