Decision Procedures for Recursive Data Structures with Integer Arithmetic

Опубликовано 6 сентября 2016, 6:25

Decision procedures exists for many specialized logical domains as well as for many data structures frequently appearing in programs. Programs, even very simple kind, however, often involve multiple data domains, resulting in verification conditions spanning more than one logical theories. Hence for modeling and analyzing high-level programs we need decision procedures which can reason about complex domains. In this talk we presents novel solutions to an important class of decision problems, the mixed constraints on data structures with constraints on ``integral measures'' of those data structures. Such constraints can express memory safety properties such as absence of memory overflow and out-of-bound array access, which are crucial for program correctness. Our approach is to reduce constraints on data structures to constraints on integers, and with presence of quantifiers, to reduce quantifiers on data objects to quantifiers on integers. We present three contributions with case studies. 1. Decision procedures for the theory of term algebras with integer constraints. This theory can express mixed constraints on tree-like data structures with integer constraints on those data structures. As an example, we show how verification conditions of the red-black tree algorithm can be expressed in this theory. 2. Decision procedures for the first-order theory of Knuth-Bendix orders. Using the reduction technique developed for the decision problem of term algebras with integer arithmetic, we proved the decidability of the first-order theory of Knuth-Bendix Order, thereby solving a long-standing open problem in term rewriting (officially listed as RTA open problem 99 since 2000). 3. Decision procedures for queues with integer constraints. We adapt the reduction technique to reason about linear data structures with integer constraints. We show semantics of most common string operations in C language can be precisely expressed in this theory and its extensions.