Automated Software Analysis Group

Debugging Overconstrained Declarative Models Using Unsatisfiable Cores

  • Author:

    Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, Mana Taghdiri

  • Place:

    International Conference on Automated Software Engineering (ASE), 2003. (distinguished paper award)

  • Date: Oct. 2003
  • 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.

BibTex

@InProceedings{shlyakhter-etal-2003,
    author    = "I. Shlyakhter and R. Seater and D. Jackson and M. Sridharan and M. Taghdiri",
    title     = {Debugging Declarative Models Using Unsatisfiable Core},
    booktitle = {18th International Conference on Automated Software Engineering (ASE)},
    pages     = {94-105},
    year      = {2003}   
}