18th IEEE International Conference on Automated Software Engineering, 2003. Proceedings. (2003)
Montreal, Quebec, Canada
Oct. 6, 2003 to Oct. 10, 2003
Ilya Shlyakhter , MIT CSAIL, Cambridge, MA
Robert Seater , MIT CSAIL, Cambridge, MA
Daniel Jackson , MIT CSAIL, Cambridge, MA
Manu Sridharan , UC Berkeley, Berkeley, CA
Mana Taghdiri , MIT CSAIL, Cambridge, MA
Declarative models, in which conjunction and negation are freely used, are susceptible to unintentional overconstraint. Core extraction is a new analysis that mitigates this problem in the context of a checker based on reduction to SAT. It exploits a recently developed facility of SAT solvers that provides an "unsatisfiable core" of an unsatisfiable set of clauses, often much smaller than the clause set as a whole. The unsatisfiable core is mapped back into the syntax of the original model, showing the user fragments of the model found to be irrelevant. This information can be a great help in discovering and localizing overconstraint, and in some cases pinpoints it immediately. The construction of the mapping is given for a generalized modelling language, along with a justification of the soundness of the claim that the marked portions of the model are irrelevant. Experiences in applying core extraction to a variety of existing models are discussed.
M. Taghdiri, I. Shlyakhter, R. Seater, D. Jackson and M. Sridharan, "Debugging Overconstrained Declarative Models Using Unsatisfiable Cores," 18th IEEE International Conference on Automated Software Engineering, 2003. Proceedings.(ASE), Montreal, Quebec, Canada, 2003, pp. 94.