| Presentation | 2003/12/12 A Bounded Model Checking Method based on Quantifier-Free Presburger Arithmetics Takahiro TANAKA, Tatsuhiro TSUCHIYA, Tohru KIKUNO, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Symbolic model checking is an automatic technique for verifying a system modeled as a state machine by the manipulation of boolean formulas. Bounded model checking, a symbolic model checking technique based on SAT procedures, has been successful in verification of hardware systems. This technique, however, does not work efficiently for software systems such as concurrent programs. In this report, we propose a bounded model checking method based on Quantifier-Free Presburger Arithmetics to achieve efficient verification for such software systems. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Bounded Model Checking / Satisfiability Decision / Quantifier-Free Presburger |
| Paper # | DC2003-79 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2003/12/12(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 | Dependable Computing (DC) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Bounded Model Checking Method based on Quantifier-Free Presburger Arithmetics |
| Sub Title (in English) | |
| Keyword(1) | Bounded Model Checking |
| Keyword(2) | Satisfiability Decision |
| Keyword(3) | Quantifier-Free Presburger |
| 1st Author's Name | Takahiro TANAKA |
| 1st Author's Affiliation | Graduate School of Information Science and Technology, Osaka University() |
| 2nd Author's Name | Tatsuhiro TSUCHIYA |
| 2nd Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| 3rd Author's Name | Tohru KIKUNO |
| 3rd Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| Date | 2003/12/12 |
| Paper # | DC2003-79 |
| Volume (vol) | vol.103 |
| Number (no) | 535 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |