|
Published Articles >> Table of Contents >> Abstract
18th IEEE International Conference on Automated Software Engineering (ASE'03)
p. 94
Debugging Overconstrained Declarative Models Using Unsatisfiable Cores
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
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2003.1240298
Send link to a friend
| Abstract |
|
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.
|
 Additional Information
|
Citation:
Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, Mana Taghdiri,
"Debugging Overconstrained Declarative Models Using Unsatisfiable Cores,"
ase,
p. 94,
18th IEEE International Conference on Automated Software Engineering (ASE'03),
2003
|
|
