JasperGold bounded model checker [Google Scholar] Papers related to JasperGold bounded model checker End-to-end formal verification of a RISC-V processor extended with capability pointers [gao:fmcad:2021]