X-IronPort-MID: 216248488
X-SBRS: 3.5
X-BrightmailFiltered: true
X-Ironport-AV: i="3.85,134,1094446800"; 
   d="scan'208"; a="216248488:sNHT12353344"
Date: Mon, 11 Oct 2004 18:58:42 -0500 (CDT)
From: Qiang Zhang 
To: acl2-mtg@lists.cc.utexas.edu
Subject: ACL2 Meeting 
Content-Type: TEXT/PLAIN; charset=US-ASCII
Reply-To: acl2-mtg@lists.cc.utexas.edu
Sender: owner-acl2-mtg@lists.cc.utexas.edu
X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
X-SpamAssassin-Status: No, hits=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-302 required=180

Greeting all!

This Wednesday, I will present my work on proving the correctness of
Dijkstra's shortest path algorithm.

Dijkstra's shortest path algorithm is a classical graph algorithm to find
the shorest path between two vertices in a finite graph with non-negative
weighted edges. The traditional proof on its correctness is not hard, but
the mechanically checked proof is somewhat tricky. I formalize the
algorithm in ACL2, and mechanically prove its correctness in ACL2.

best regards,
Qiang