[isabelle] Graph algorithms


Almost two  years ago I asked  a question about  graph algorithms that
had  been  verified formally.  The  replies  that  I have  gotten  are
summarized below.

In  the meantime,  Gilbert Lee  finished his  MSc thesis  in  which he
proved  in Mizar  Dijkstra's  SSSP, Prim's  MST and  Floyd-Fulkerson's
flow.  All  done at the level  of graph operations.  His  thesis is at
http://www.cs.ualberta.ca/~piotr/Mizar/ and the  Mizar articles are at

Another  student  of  mine,   Broderic  Arneson,  is  now  formalizing
algorithms on  chordal graphs following  Golumbic's "Algorithmic Graph
Theory and Perfect Graphs".  If  you know of any effort in formalizing
similar material (or something new in graph theory in general) please
let me know.


Piotr Rudnicki        CompSci, University of Alberta, Edmonton, Canada


     Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya,
     Shin-ya Nishizaki and Tetsuo Tamai:
     Formalization of Graph Search Algorithms and Its Applications,
     Theorem Proving in Higher Order Logics,
     11th International Conference, TPHOLs'98,
     Canberra, Australia, September/October 1998, Proceedings
     (Jim Grundy, Malcolm Newey, eds.)
     Lecture Notes in Computer Science, Springer-Verlag, Vol.1479, 1998,


     With Jean-Raymond Abrial and Dominique M?ry we have developed
     and proved mechanically Prim's MST algorithm. You can find our paper 
     on this web page.


     In ACL2

     ;A mechanically checked proof of Dijkstra's shortest-path alogrithm
     ;Qiang Zhang      (qzhang at cs.utexas.edu)
     ;J Strother Moore (moore at cs.utexas.edu)


     Ranan Fraer did something a while ago with the B method:


     In Mizar

     :: Dijkstra's Shortest Path Algorithm
     ::  by Jing-Chao Chen
     :: Received March 17, 2003
     :: Copyright (c) 2003 Association of Mizar Users


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.