Cutting the Cake Into Crumbs: Verifying Envy-Free Cake-Cutting Protocols using Bounded Integer Arithmetic

Explore a conference talk that delves into the verification of envy-free cake-cutting protocols using bounded integer arithmetic. Learn about fair division protocols for splitting continuous resources among multiple agents with varying preferences, and discover how envy-free protocols ensure no agent prefers another's allocation. Examine the complexities of these protocols and the potential errors in manual proofs of correctness. Investigate the recent development of the DSL Slice for describing protocols and the reduction of envy-freeness verification to SMT instances in quantified non-linear real arithmetic. Understand the limitations of this approach and explore a new method that proves counterexamples to envy-freeness can be found with bounded integer arithmetic under reasonable assumptions. Discover how an embedded DSL for describing cake-cutting protocols in declarative-style C, combined with the bounded model-checker CBMC, reduces envy-freeness verification to checking unsatisfiability of pure SAT instances, resulting in significant improvements in verification time for unfair protocols.

[PADL'24] Cutting the Cake Into Crumbs: Verifying Envy-Free Cake-Cutting Protocols using B...