Abstract
We develop a certified decision procedure for reasoning about systems of equations over the "tree share" fractional permission model of Dockins et al. Fractional permissions provide a principled way to reason about shared ownership of resources, particularly in concurrent programs. We formally verified our decision procedure and integrated it into the HIP/SLEEK verification system. During integration, we discovered bugs in both the previous uncertified decision procedure and HIP/SLEEK itself. Beyond certification, our new procedure improves prior work by correctly handling negative clauses and achieving better performance.