Trustworthy Verification of RISC-V Binaries Using Symbolic Execution in HolBA

Karl Palmskog, Andreas Lindner, Scott Constable +2

Many types of formal verification establish properties about abstract high-level program representations, leaving a large gap to programs at runtime. Although gaps can sometimes be…