Abstract
This paper describes a formalization of a class of fixed-point problems on graphs and its applications. This class captures several well-known graph theoretical problems such as those of shortest path type and for data flow analysis. An abstract solution algorithm of the fixed-point 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 proof of the latter. The insights we obtained through these formalizations are described. We also discuss the extension of this approach to the verification of model checking algorithms.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
David Basin and Matt Kaufmann. The Boyer-Moore prover and Nuprl: An experimental comparison. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 89–119. Cambridge University Press, 1991.
Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, New York, 1979.
Albert J. Camilleri and Wishnu Prasetya. Cpo theory, 1994. Available from http://www.cl.cam.ac.uk/ftp/hvg/hol88/contrib/cpo/.
C.-T. Chou. A formal theory of undirected graphs in higher-order logic. In Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 859 of LNCS, pages 144–157, Valletta, Malta, September 1994. Springer-Verlag.
Ching-Tsun Chou and Doron Peled. Verifying a model-checking algorithm. In Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in LNCS, pages 241–257, Passau, Germany, 1996. Springer-Verlag.
A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
E. Allen Emerson. Handbook of Theoretical Computer Science, chapter 16. Elsevier Science Publishers B.V., 1990.
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
R. HÄhnle, M. Heisel, W. Reif, and W. Stephan. An interactive verification system based on dynamic logic. In J. Seikmann, editor, 8th International Conference on Automated Deduction, number 230 in LNCS, pages 306–315, Oxford, 1986. Springer-Verlag. Also note etsehttp://www.informatik.uni-ulm.de/pm/kiv/kiv.htmletse.
Wim H. Hesselink. The verified incremental design of a distributed spanning tree algorithm — extended abstract. Computing Science Reports Groningen CS-R9602, November 1997. Available from http://www.cs.rug.nl/~wim/ghs/whh168.ps.
G. Kildall. A unified approach to global program optimization. In POPL, pages 194–206, 1973.
Bruno Martin, July 1997. Private Communication.
Nils J. Nilsson. Principles of Artificial Intelligence. Tioga Publishing, 1980.
N. Shankar, S. Owre, and J. Rushby. The PVS proof checker: A reference manual. Technical report, Computer Science Lab, SRI Intl., 1993.
Tetsuo Tamai. A class of fixed-point problems on graphs and iterative solution algorithms. In Logic and Software Engineering, pages 102–121. World Scientific, 1996.
P. Windley. Abstract theories in HOL. In Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 Workshop, volume A-20 of IFIP Transactions, pages 197–210, Leuven, Belgium, September 1992. North-Holland/Elsevier.
W. Wong. A simple graph theory and its application in railway signalling. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 395–409, Davis, California, USA, August 1991. IEEE Computer Society Press, 1992.
Mitsuharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya, and Yozo Toda. Formalization of planar graphs. In 8th International Workshop on Higher-Order Logic Theorem Proving and Its Applications, volume 971 of LNCS, pages 369–384. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yamamoto, M., Takahashi, K., Hagiya, M., Nishizaki, Sy., Tamai, T. (1998). Formalization of graph search algorithms and its applications. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055153
Download citation
DOI: https://doi.org/10.1007/BFb0055153
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64987-8
Online ISBN: 978-3-540-49801-8
eBook Packages: Springer Book Archive