Decision procedures for region logic

Stan Rosenberg, Anindya Banerjee, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

6 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
Pages379-395
Number of pages17
DOIs
StatePublished - 2012
Event13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012 - Philadelphia, PA, United States
Duration: 22 Jan 201224 Jan 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7148 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
Country/TerritoryUnited States
CityPhiladelphia, PA
Period22/01/1224/01/12

Fingerprint

Dive into the research topics of 'Decision procedures for region logic'. Together they form a unique fingerprint.

Cite this