Push-relabel algoritmi formaalne tõestamine Coq raamistikus
Nimi
Aksel Õim
Kokkuvõte
Push-relabel algoritm arvutab transpordivõrgus välja maksimaalse voo, andes tippudele kõrgused ja ülejäägid. Algoritm üritab tippudes olevat ülejääki saata väljundisse, muutes vajadusel tippude kõrguseid ja samal ajal säilitades kolme erinevat invarianti. Bakalaureusetöö eesmärk on formaalselt tõestada Coq raamistikus push-relabel algoritm, andes ülevaate algoritmi implementatsioonist ja tõestatud lemmadest. Keskendutakse algoritmi tõestamisele, kuid tutvustakse Coq raamistikku, graafi mõisteid ja kirjeldatakse push-relabel algoritmi tööd.
Lõputöö keel
eesti
Lõputöö tüüp
Bakalaureus - Informaatika
Juhendaja(d)
Kalmer Apinis
Kaitsmise aasta
2024