| Presentation | 2015-03-06 Development of SMT-based model checker for assembly codes using an interrupt reduction technique Jumpei KOBASHI, Atsushi TAKESHITA, Satoshi YAMANE, Kohei SAKURAI, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Recently, embedded software has 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 a formal verification with SMT-Based Bounded Model Checking (SMT-Based BMC) for embedded assembly codes. Our proposed method generates models of assembly codes in detail with the fixed-sized bit-vectors theory. The models generated by our method include interrupts and reduces the size of the models using Interrupt Handler Execution Reduction (IHER) technique. In this paper, we have developed an automatic model checker using our method. Moreover, we show the validity of our method by experiments. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Formal Verification / Program Checking / Assembler Language / SMT-Based BMC / Bounded Model Checking |
| Paper # | MSS2014-100 |
| Date of Issue |
| Conference Information | |
| Committee | MSS |
|---|---|
| Conference Date | 2015/2/26(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Mathematical Systems Science and its applications(MSS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Development of SMT-based model checker for assembly codes using an interrupt reduction technique |
| Sub Title (in English) | |
| Keyword(1) | Formal Verification |
| Keyword(2) | Program Checking |
| Keyword(3) | Assembler Language |
| Keyword(4) | SMT-Based BMC |
| Keyword(5) | Bounded Model Checking |
| 1st Author's Name | Jumpei KOBASHI |
| 1st Author's Affiliation | Kanazawa University() |
| 2nd Author's Name | Atsushi TAKESHITA |
| 2nd Author's Affiliation | Kanazawa University |
| 3rd Author's Name | Satoshi YAMANE |
| 3rd Author's Affiliation | Kanazawa University |
| 4th Author's Name | Kohei SAKURAI |
| 4th Author's Affiliation | Kanazawa University |
| Date | 2015-03-06 |
| Paper # | MSS2014-100 |
| Volume (vol) | vol.114 |
| Number (no) | 493 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |