A Certified Decision Procedure for Tree Shares

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.

Cite this paper

@inproceedings{le2017certified,
  author    = {Le, Xuan-Bach and Nguyen, Thanh-Toan and Chin, Wei-Ngan and Hobor, Aquinas},
  title     = {A Certified Decision Procedure for Tree Shares},
  booktitle = {Formal Methods and Software Engineering (ICFEM 2017)},
  pages     = {226--242},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  isbn      = {978-3-319-68690-5},
  year      = {2017},
  doi       = {10.1007/978-3-319-68690-5_14}
}