Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Graph algorithms


view this post on Zulip Email Gateway (Aug 17 2022 at 13:45):

From: Piotr Rudnicki <piotr@cs.ualberta.ca>
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,


Last updated: May 03 2024 at 04:19 UTC