Dominique Gückel, I11
|Title||A System for Synthesizing Abstraction-Enabled Simulators for Binary Code Verification|
|Where||Lecture Room Informatik 11|
|Abstract||Formal verification of embedded software is crucial in safety-critical applications. In the ideal case, the verification is conducted automatically
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.
- Subscribe to the ics feed.
- No Events