Converting programs into constraint satisfaction problems

Abstract

In this paper we introduce the basic methodology for analyzing and debugging programs. We first convert programs into their loop-free equivalents and from this into the static single assignment form. From the static single assignment form we derive a corresponding constraint satisfaction problem. The constraint representation can be directly used for debugging. From the corresponding hyper-tree representation of the constraint satisfaction problem we compute the hyper-tree width which characterizes the complexity of finding a solution for the constraint satisfaction problem. Since constraint satisfaction can be effectively used for diagnosis the conversion can be used for debugging and the obtained hyper-tree width is an indicator of the debugging complexity. © 2008 Springer-Verlag Berlin Heidelberg.