Model generation by the exhaustive search for embedded assembly programs and application to model checking
Ryousuke Konoshita, Kouhei Sakurai, Satoshi Yamane · 2014
Embedded systems have been widely used. Therefore, it is important to ensure the safety. Model checking is effective to ensure the safety for systems. We have developed Behavior Extractor to model the behavior of embedded assembly programs automatically. The model is used for model checking. In addition, we have introduced the undefined value to reduce the number of states.