Bounded Model Checking of RISC-V Machine Code with Context-Free-Language Ordered Binary Decision Diagrams

Anna Bolotina, Christoph M. Kirsch, Stefanie Muroya Lei +1

Symbolic execution is a powerful technique for analyzing the behavior of software yet scalability remains a challenge due to state explosion in control and data flow. Existing tool…