A system for synthesizing abstraction-enabled simulators for binary code verification

Formal verification of embedded software is crucial in safety-critical applications, ideally requiring as little human intervention as possible. 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. In the embedded systems domain with its varieties of different architectures in use, this can severely restrict the applicability of this approach. To remedy this drawback, we describe a system for automatically synthesizing simulators, which are suited for model checking in that they support automatic abstraction. We evaluate the practicality of this approach by synthesizing simulators for the Atmel ATmega16 and Intel MCS-51 microcontrollers.