Cutting the Cake Into Crumbs: Verifying Envy-Free Cake-Cutting Protocols using B...
summary
Proves that any counterexample to envy-freeness for a bounded finite cake‑cutting protocol can be found using bounded integer arithmetic rather than slow real SMT; constructs an embedded DSL called crumbs in declarative C that models slices as integer “crumbs” per focused agent; compiles protocols to SAT via CBMC + KISSAT and checks envy by asserting other agents’ totals ≤ focused agent’s total; reports drastic speedups for finding envy (sat) cases, with verification of fairness (unsat) remaining harder.
AI-written summary · about
chapters (7)
- 0:00Cake-cutting fairness
- 7:07Previous work
- 10:39Crumbs DSL for verification
- 16:39Implementation details
- 20:09Empirical results
- 22:56Summary and future work
- 24:09Q&A
related talks
14mDivide and Conquer: A Compositional Approach to Game-Theoretic Security
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
32mSymbolic analysis by using folding narrowing with irreducibility and SMT constra...
28mNotes from the SNARKonomicon: Techniques for Writing SNARK Programs
33mA Wishlist for Verifiable Computation: An Applied CS Perspective
24mAutomated game-theoretic security analysis of blockchain protocols
31mSequential Composition of Rational Proofs
15mCore slicing: closing the gap between leaky confidential VMs and bare-metal cloud