Title
Formalization of Graph Search Algorithms and Its Applications
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 Yamamoto19111.09
Koichi Takahashi2386.30
Masami Hagiya3649102.85
Shin-ya Nishizaki4389.21
Tetsuo Tamai533433.27