Cutting the Cake into Crumbs: Verifying Envy-Free Cake-Cutting Protocols Using Bounded Integer Arithmetic

Fair division protocols specify how to split a continuous resource (conventionally represented by a cake) between multiple agents with different preferences. Envy-free protocols ensure no agent prefers any other agent's allocation to his own. These protocols are complex and manual proofs of their correctness may contain errors. Recently, Bertram and others [5] developed the DSL Slice for describing these protocols and showed how verification of envy-freeness can be reduced to SMT instances in the theory of quantified non-linear real arithmetic. This theory is decidable, but the decision procedure is slow, both in theory and in practice. We prove that, under reasonable assumptions about the primitive operations used in the protocol, counterexamples to envy-freeness can always be found with bounded integer arithmetic. Building on this result, we construct an embedded DSL for describing cake-cutting protocols in declarative-style C. Using the bounded model-checker CBMC, we reduce verifying envy-freeness of a protocol to checking unsatisfiability of pure SAT instances. This leads to a substantial reduction in verification time when the protocol is unfair.