/coq-wigderson

Formalization of Wigderson's graph coloring algorithm in Coq

Primary LanguageCoqMIT LicenseMIT

Formal Verification of Modified Version of Wigderson's Algorithm for 3-colorable graphs.

Created by: Ben Siraphob (siraben) and Jamison Homatas (jhomatas48)

We present a formal proof of an approximate a coloring for 3-colorable graphs. Our algorithm is based upon Avi Wigderson's algorithm, and we have modified this to be more explicit and rigorous. We implement this as a functional program in Gallina. This repo includes definitions for graphs and graph components and all other data structures used. See the attached paper for more information.

Using Nix, run nix-shell then run make to compile it.

License

This software is licensed under the MIT license.