BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalisation of Combinatorial Optimisation in Isabelle/HOL: Netwo
 rk Flows - Thomas Ammer (King's College London)
DTSTART:20250206T170000Z
DTEND:20250206T180000Z
UID:TALK224908@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:Combinatorial optimisation (CO) is a sub-area of discrete math
 ematics. Basic examples for CO problems are finding a shortest path or a m
 inimum spanning tree in a graph. So-called network flows or variations of 
 matching would be more advanced problems. There are also abstract concepts
  like matroids that offer an algebraic point of view and a uniform foundat
 ion for some of the more concrete problems.\n\nSince the considered struct
 ures are finite\, it is a natural aim to compute a solution efficiently. T
 hat implies an overlap with the theory of algorithms\, especially running 
 time analysis. \n\nThis talk is mainly about the Isabelle/HOL formalisatio
 n of a specific CO problem\, namely\, minimum cost flows\, which are a sub
 type of network flows. Among others\, this includes Orlin's Algorithm\, wh
 ich is a most efficient method to compute a minimum cost flow in general n
 etworks. Also\, the running time argument for this advanced algorithm and 
 some reductions among flow problems were formalised. \n\n- The Isabelle pr
 oof scripts can be found in this GitHub repo: https://github.com/mabdula/I
 sabelle-Graph-Library\n\n- The formalisation is described in this paper: A
  Formal Analysis of Capacity Scaling Algorithms for Minimum Cost Flows by 
 Mohammad Abdulaziz and Thomas Ammer\, ITP 2024\n\n\n=== Hybrid talk ===\n\
 nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVr
 IE1IppYCsbooOVqenzI.1\n\nMeeting ID: 871 4336 5195\n\nPasscode: 541180
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR