| Paper Abstract and Keywords |
| Presentation |
2007-11-20 11:20
An Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
Hiroaki Shimizu, Kiyoharu Hamaguchi, Toshinobu Kashiwabara (Osaka Univ.) |
| Abstract |
(in Japanese) |
(See Japanese page) |
| (in English) |
Model checking technique, which is a method to verify systems automatically, have attracted attentions. Model checking, however, cannot be applied to systems which are large or complicated. To handle this problem, abstraction techniques using a subset of first-order logic, called EUF, have been proposed, but a model checking using EUF is generally undecidable. In this report, we introduce a method to terminate state enumeration by using term-height reduction. Finally we show an overapproximate algorithm which can check if a designated invariant always holds for the system. Furthermore, we show an example of application of our algorithm to simple hardware designs. |
| Keyword |
(in Japanese) |
(See Japanese page) |
| (in English) |
model checking / first-order logic / abstraction / invariant / / / / |
| Reference Info. |
IEICE Tech. Rep., vol. 107, pp. 19-24, Nov. 2007. |
| Paper # |
|
| Date of Issue |
2007-11-13 (VLD, DC) |
| ISSN |
Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 |
| Download PDF |
|
| Conference Information |
| Committee |
VLD CPSY RECONF DC IPSJ-SLDM IPSJ-ARC |
| Conference Date |
2007-11-20 - 2007-11-22 |
| Place (in Japanese) |
(See Japanese page) |
| Place (in English) |
Kitakyushu International Conference Center |
| Topics (in Japanese) |
(See Japanese page) |
| Topics (in English) |
Design Gaia 2007 ---A New Frontier in VLSI Design--- |
| Paper Information |
| Registration To |
IPSJ-SLDM |
| Conference Code |
2007-11-VLD-CPSY-RECONF-DC-IPSJ-SLDM-IPSJ-ARC |
| Language |
Japanese |
| Title (in Japanese) |
(See Japanese page) |
| Sub Title (in Japanese) |
(See Japanese page) |
| Title (in English) |
An Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic |
| Sub Title (in English) |
|
| Keyword(1) |
model checking |
| Keyword(2) |
first-order logic |
| Keyword(3) |
abstraction |
| Keyword(4) |
invariant |
| Keyword(5) |
|
| Keyword(6) |
|
| Keyword(7) |
|
| Keyword(8) |
|
| 1st Author's Name |
Hiroaki Shimizu |
| 1st Author's Affiliation |
Osaka University (Osaka Univ.) |
| 2nd Author's Name |
Kiyoharu Hamaguchi |
| 2nd Author's Affiliation |
Osaka University (Osaka Univ.) |
| 3rd Author's Name |
Toshinobu Kashiwabara |
| 3rd Author's Affiliation |
Osaka University (Osaka Univ.) |
| 4th Author's Name |
|
| 4th Author's Affiliation |
() |
| 5th Author's Name |
|
| 5th Author's Affiliation |
() |
| 6th Author's Name |
|
| 6th Author's Affiliation |
() |
| 7th Author's Name |
|
| 7th Author's Affiliation |
() |
| 8th Author's Name |
|
| 8th Author's Affiliation |
() |
| 9th Author's Name |
|
| 9th Author's Affiliation |
() |
| 10th Author's Name |
|
| 10th Author's Affiliation |
() |
| 11th Author's Name |
|
| 11th Author's Affiliation |
() |
| 12th Author's Name |
|
| 12th Author's Affiliation |
() |
| 13th Author's Name |
|
| 13th Author's Affiliation |
() |
| 14th Author's Name |
|
| 14th Author's Affiliation |
() |
| 15th Author's Name |
|
| 15th Author's Affiliation |
() |
| 16th Author's Name |
|
| 16th Author's Affiliation |
() |
| 17th Author's Name |
|
| 17th Author's Affiliation |
() |
| 18th Author's Name |
|
| 18th Author's Affiliation |
() |
| 19th Author's Name |
|
| 19th Author's Affiliation |
() |
| 20th Author's Name |
|
| 20th Author's Affiliation |
() |
| Speaker |
Author-1 |
| Date Time |
2007-11-20 11:20:00 |
| Presentation Time |
25 minutes |
| Registration for |
IPSJ-SLDM |
| Paper # |
VLD2007-73, DC2007-28 |
| Volume (vol) |
vol.107 |
| Number (no) |
no.334(VLD), no.337(DC) |
| Page |
pp.19-24 |
| #Pages |
6 |
| Date of Issue |
2007-11-13 (VLD, DC) |
|