Abstract | ||
---|---|---|
This paper describes a formalization of a class of fixed-point problems on graphs and its applications. This class captures several wellknown graph theoretical problems such as those of shortest path type and for data flow analysis. An abstract solution algorithm of the fixedpoint problem is formalized and its correctness is proved using a theorem proving system. Moreover, the validity of the A* algorithm, considered as a specialized version of the abstract algorithm, is proved by extending the ... |
Year | DOI | Venue |
---|---|---|
1998 | 10.1007/BFb0055153 | TPHOLs |
Keywords | Field | DocType |
graph search algorithms,data flow analysis,fixed point,theorem proving,shortest path | Program optimization,Discrete mathematics,Model checking,Search algorithm,Shortest path problem,Computer science,Correctness,Data-flow analysis,Theorem Proving System,Algorithm,Theoretical computer science,Formal verification | Conference |
Volume | ISSN | ISBN |
1479 | 0302-9743 | 3-540-64987-5 |
Citations | PageRank | References |
8 | 0.68 | 8 |
Authors | ||
5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Mitsuharu Yamamoto | 1 | 91 | 11.09 |
Koichi Takahashi | 2 | 38 | 6.30 |
Masami Hagiya | 3 | 649 | 102.85 |
Shin-ya Nishizaki | 4 | 38 | 9.21 |
Tetsuo Tamai | 5 | 334 | 33.27 |