Abstract
Fractional permissions enable sophisticated management of resource access in both sequential and concurrent programs. Entailment checkers for separation logic formulas containing fractional permissions must therefore reason precisely about such permissions. We show how entailment checkers for separation logic with fractional permissions can extract equation systems over fractional shares. We develop a set of decision procedures for equations arising from the sophisticated Boolean binary tree fractional permission model of Dockins et al. We prove that our procedures are sound and complete and analyze their computational complexity. We describe our implementation, provide performance benchmarks, and detail its integration into the HIP/SLEEK verification toolset. Our results are supported by machine-checked proofs in Coq.