| Presentation | 2002/4/12 Implementing a SAT-Based Model Checking Tool 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 finite state machine by the manipulation of boolean formulas. Recently, a SAT-based symbolic model checking technique, called bounded model checking, was proposed. In this paper, we describe our model checking tool implementing this technique. The basic idea of the method is to consider a counterexample of a particular length k and generate a propositional formula that is satisfisble if such a counterexample exists. Theoretically the model checking technique can deal with LTL (linear temporal logic) specifications, and BMC, a tool based on this technique, has already been publically available; however, the current version of this tool can verify simple safety and liveness properties only. In contrast, our tool can verify arbitrary LTL formulas. The result of a case study shows that our tool can be used as an alternative when traditional BDD-based symbolic model checking cannot work efficiently. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Bounded model checking / satisfiability decision / linear temporal logic |
| Paper # | DC2002-1 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2002/4/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) | Implementing a SAT-Based Model Checking Tool |
| Sub Title (in English) | |
| Keyword(1) | Bounded model checking |
| Keyword(2) | satisfiability decision |
| Keyword(3) | linear temporal logic |
| 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 | 2002/4/12 |
| Paper # | DC2002-1 |
| Volume (vol) | vol.102 |
| Number (no) | 28 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |