Round-Robin Scheduler Verification in Coq

A Formal Verification of Scheduling Properties

This project implements and formally verifies a Round-Robin CPU scheduling algorithm using the Coq Proof Assistant.
It models a simplified job scheduling system and provides proofs of correctness, termination, and fairness properties grounded in mathematical logic.

---

⚙️ Overview

The project defines a minimal representation of jobs—each with an identifier and a burst time—and simulates how these jobs are processed in a round-robin manner based on a fixed time quantum.
It introduces foundational axioms, lemmas, and theorems that collectively prove the algorithm’s soundness.

---

📘 Key Features

• 🧩 Formal definition of jobs, job lists, and scheduling operations
• ⚙️ Implementation of a Round-Robin scheduler (rr_sched)
• 📏 Proven properties, including:
  • ✅ Finite termination – guarantees all jobs complete
  • ✅ No starvation – every job gets CPU time
  • ✅ Fairness – all jobs are scheduled equally
• 💻 Written entirely in Coq, with clear logical structure and proofs

---

🧠 Example Output

Compute example_output.
(* OUTPUT : = ([], [1; 2; 3; 1; 2; 3]) *)