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 can reason about shared ownership of resources, e.g. in a concurrent program. We imported our certified procedure into the HIP/SLEEK verification system and found bugs in both the previous, uncertified, decision procedure and HIP/SLEEK itself. In addition to being certified, our new procedure improves previous work by correctly handling negative clauses and enjoys better performance.
CITATION STYLE
Le, X. B., Nguyen, T. T., Chin, W. N., & Hobor, A. (2017). A Certified Decision Procedure for Tree Shares. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10610 LNCS, pp. 226–242). Springer Verlag. https://doi.org/10.1007/978-3-319-68690-5_14
Mendeley helps you to discover research relevant for your work.