coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Graph algorithms

From: Piotr Rudnicki <piotr AT cs.ualberta.ca>
To: QED-like <qed AT mcs.anl.gov>, coq-club AT pauillac.inria.fr, info-hol AT phirewall.cs.byu.edu, isabelle-users AT cl.cam.ac.uk, imps AT hygelac.cas.mcmaster.ca, nuprllist AT cs.cornell.edu, pvs AT csl.sri.com, nqthm-users AT cs.utexas.edu, nuprl AT cs.cornell.edu
Subject: [Coq-Club]Graph algorithms
Date: Wed, 18 Jan 2006 16:22:54 -0700
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello,

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
www.mizar.org.

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.

Sincerely,

--
Piotr Rudnicki        CompSci, University of Alberta, Edmonton, Canada
                      http://web.cs.ualberta.ca/~piotr

--------------------------

     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,
     pp.479-496.

--------------------------

     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.

http://springerlink.metapress.com/app/home/contribution.asp?wasp=g3twnwwhwj0854qmhqvl&referrer=parent&backto=issue,27,31;journal,361,1541;linkingpublicationresults,1:105633,1

--------------------------

     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:
     http://citeseer.ist.psu.edu/fraer97derivation.html

--------------------------

     In Mizar

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

--------------------------

[Coq-Club]Graph algorithms, Piotr Rudnicki