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 that 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 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.

I received my undergraduate degree in Computer Science from the University of Cambridge. I completed a master’s degree, doctorate and postdoc at the University of Oxford. My thesis was on information flow and metaprogramming, considering specifically the eval construct as found in JavaScript. Since September 2018, I have been a lecturer at the University of Reading.