An empirical study of structural constraint solving techniques

J. H. Siddiqui and S. Khurshid
International Conference on Formal Engineering Methods (ICFEM 2009)

Abstract

Structural constraint solving allows finding object graphs that satisfy given constraints, thereby enabling software reliability tasks, such as systematic testing and error recovery. Since enumerating all possible object graphs is pro- hibitively expensive, researchers have proposed a number of techniques for re- ducing the number of potential object graphs to consider as candidate solutions. These techniques analyze the structural constraints to prune from search object graphs that cannot satisfy the constraints. Although, analytical and empirical eval- uations of individual techniques have been done, comparative studies of different kinds of techniques are rare in the literature. We performed an experiment to evaluate the relative strengths and weaknesses of some key structural constraint solving techniques. The experiment considered four techniques using: a model checker, a SAT solver, a symbolic execution engine, and a specialized solver. It focussed on their relative abilities in expressing the constraints and formatting the output object graphs, and most importantly on their performance. Our results highlight the tradeoffs of different techniques and help choose a technique for practical use.
(ICFEM 2009), Rio de Janeiro, Brazil, December 2009. (Acceptance rate: 29%, 36/121)

BibTex

@inproceedings { icfem2009,
author = { }, }