| Presentation | 2011-10-28 Towards a formal verification of interrupts in TOPPERS/ASP by the separation logic Takashi NAKASHIMA, Shoji YUEN, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | We give a formal verification of a fragment of ARM assembly code in TOPPERS/ASP to handle interrupts using the separation logic. Since an ARM processor switches the function of registers according to the processor modes, we need to trace memory usage in order to verify behavior. By giving a proof for the code fragment involving interrupt handling, it is shown that pre-conditions and post-conditions are explicitly presented to make the assembly code work correctly. The purpose of this study is formally verifying that behavior of existing OS is what the programmer intended. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Separation Logic / ARM processor / formal verification / assembly language |
| Paper # | SS2011-37 |
| Date of Issue |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2011/10/20(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 | Software Science (SS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Towards a formal verification of interrupts in TOPPERS/ASP by the separation logic |
| Sub Title (in English) | |
| Keyword(1) | Separation Logic |
| Keyword(2) | ARM processor |
| Keyword(3) | formal verification |
| Keyword(4) | assembly language |
| 1st Author's Name | Takashi NAKASHIMA |
| 1st Author's Affiliation | Graduate School of Information Science, Nagoya University() |
| 2nd Author's Name | Shoji YUEN |
| 2nd Author's Affiliation | Graduate School of Information Science, Nagoya University |
| Date | 2011-10-28 |
| Paper # | SS2011-37 |
| Volume (vol) | vol.111 |
| Number (no) | 268 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |