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 ZhangTo: 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