A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification

Dominique Gückel, I11

with little or no human intervention. Binary code model checking based on hardware simulators already comes close to this goal, although with high initial effort for developing a simulator of the respective target platform. We present results from a recent publication in which we describe how to remedy this drawback. The presentation focuses on two aspects: first, the synthesis of microcontroller simulators for two different platforms, and second, the (automatic) integration of abstraction techniques into the synthetic simulators, which are needed to counter the state explosion problem.