| Presentation | 2015-03-06 SMT-based Model Checking for Linear Hybrid Automata using CEGAR Shohei TOMISAKA, Ryo YANASE, Kohei SAKURAI, Satoshi YAMANE, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Model Checking is the technique to verify whether the system satisfies the safety property. The Reachability analysis is a powerful technique in the verification of the safety property. However in this method, we need a solution for the state explosion problem. For this problem, Counterexample-Guided Abstraction Refinement (CEGAR) is proposed to avoid the state explosion. In this paper, we propose the technique in order to verify the safety property by the reachability analysis for hybrid systems, and we apply the CEGAR framework, and verify them using the SMT (Satisfiability Modulo Theories)-Solver. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Model Checking / state explosion / hybrid system / CEGAR / SMT-Solver |
| Paper # | MSS2014-99 |
| 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) | SMT-based Model Checking for Linear Hybrid Automata using CEGAR |
| Sub Title (in English) | |
| Keyword(1) | Model Checking |
| Keyword(2) | state explosion |
| Keyword(3) | hybrid system |
| Keyword(4) | CEGAR |
| Keyword(5) | SMT-Solver |
| 1st Author's Name | Shohei TOMISAKA |
| 1st Author's Affiliation | Kanazawa University Graduate School of Natural Science & Technology() |
| 2nd Author's Name | Ryo YANASE |
| 2nd Author's Affiliation | Kanazawa University Graduate School of Natural Science & Technology |
| 3rd Author's Name | Kohei SAKURAI |
| 3rd Author's Affiliation | Kanazawa University Graduate School of Natural Science & Technology |
| 4th Author's Name | Satoshi YAMANE |
| 4th Author's Affiliation | Kanazawa University Graduate School of Natural Science & Technology |
| Date | 2015-03-06 |
| Paper # | MSS2014-99 |
| Volume (vol) | vol.114 |
| Number (no) | 493 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |