Name
Abstract | ||
|---|---|---|
Abstract model checking has been studied as a promising technique for applying various model checking methods to infinite state systems. Graph transformation systems [11], which can model many distributed and concurrent algorithms, are examples of such infinite systems.We have been studying abstraction of several kinds of link structures, which are instances of graph transformation systems. First, we introduced abstraction of heap structures using regular expressions mainly for verifying concurrent garbage collection algorithms [14,15]. In this setting, each cell has a color and a link to another cell. Since cells can be allocated dynamically during execution, it is impossible to enumerate all the execution states of the heap. Thus we need to use abstraction for applying finite verification methods. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/978-3-540-69149-5_57 | VSTTE |
Keywords | Field | DocType |
infinite system,execution state,concurrent garbage collection algorithm,graph transformation system,various model checking method,temporal logic,finite verification method,link structure,heap structure,graph transformation systems,concurrent algorithm,abstract model checking,regular expression,model checking,graph transformation | Kripke structure,Abstraction model checking,Model checking,Programming language,Predicate abstraction,Computer science,Theoretical computer science,Heap (data structure),Graph rewriting,Garbage collection,Temporal logic | Conference |
Volume | ISSN | Citations |
4171 | 0302-9743 | 1 |
PageRank | References | Authors |
0.35 | 16 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mitsuharu Yamamoto | 1 | 91 | 11.09 |
| Yoshinori Tanabe | 2 | 124 | 13.96 |
| Koichi Takahashi | 3 | 38 | 6.30 |
| Masami Hagiya | 4 | 649 | 102.85 |