Comparative Experiment of SPIN and SMT in Model Checking of Embedded Assembly Program

Embedded software, which has properties dependent on hardware, is important for Consumer electronics. Formal verifications of embedded software are useful techniques. Our study aims at comparative experimental study of SPIN and our Satisfiability Modulo Theories -Based Bounded Model Checking (SMT-Based BMC) of Embedded Assembly Program. The models are generated by our method include interrupts. The size of the models is reduced using Interrupt Handler Execution Reduction (IHER). We can verify assembly program using SPIN in less time than using our SMT-Based BMC, but our SMT-Based BMC is convenient because it can use background theories and its general purpose theorem provers.