Development of SMT-Based Bounded Model Checker for Embedded Assembly Program

Recently, embedded assembly programs have properties dependent on hardware (direct operation of address spaces, memory mapped I/O, interruption, etc.) in the process of development. Thus, demands about the established method of formal verifications corresponding to those properties are increasing from the point of view of shorter development and high reliability. Our work aims at enabling formal verification for embedded software. We propose the detailed verification method with SMT-Based BMC for the Assembly Code Block (ACB). In addition, we have developed the automatic verification. Our method is based on the verification for the assembly program [ 1] and the verification using SMT-Based BMC for the embedded ANSI-C program [2] [3]. In this paper, we have developed the parser and the model converter for source codes of assembly program (assembly codes). Moreover, we show the validity of our method by experiments.