TY - GEN
T1 - Decision procedures for region logic
AU - Rosenberg, Stan
AU - Banerjee, Anindya
AU - Naumann, David A.
PY - 2012
Y1 - 2012
N2 - Region logic is Hoare logic for object-based programs. It features local reasoning with frame conditions expressed in terms of sets of heap locations. This paper studies tableau-based decision procedures for RL, the quantifier-free fragment of the assertion language. This fragment combines sets and (functional) images with the theories of arrays and partial orders. The procedures are of practical interest because they can be integrated efficiently into the satisfiability modulo theories (SMT) framework. We provide a semi-decision procedure for RL and its implementation as a theory plugin inside the SMT solver Z3. We also provide a decision procedure for an expressive fragment of RL termed restricted-RL. We prove that deciding satisfiability of restricted-RL formulas is NP-complete. Both procedures are proven sound and complete. Preliminary performance results indicate that the semi-decision procedure has the potential toscale to large input formulas.
AB - Region logic is Hoare logic for object-based programs. It features local reasoning with frame conditions expressed in terms of sets of heap locations. This paper studies tableau-based decision procedures for RL, the quantifier-free fragment of the assertion language. This fragment combines sets and (functional) images with the theories of arrays and partial orders. The procedures are of practical interest because they can be integrated efficiently into the satisfiability modulo theories (SMT) framework. We provide a semi-decision procedure for RL and its implementation as a theory plugin inside the SMT solver Z3. We also provide a decision procedure for an expressive fragment of RL termed restricted-RL. We prove that deciding satisfiability of restricted-RL formulas is NP-complete. Both procedures are proven sound and complete. Preliminary performance results indicate that the semi-decision procedure has the potential toscale to large input formulas.
UR - http://www.scopus.com/inward/record.url?scp=84856187426&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84856187426&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-27940-9_25
DO - 10.1007/978-3-642-27940-9_25
M3 - Conference contribution
AN - SCOPUS:84856187426
SN - 9783642279393
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 379
EP - 395
BT - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
T2 - 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
Y2 - 22 January 2012 through 24 January 2012
ER -