The Community for Technology Leaders
2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) (2003)
Montreal, Quebec, Canada
Oct. 6, 2003 to Oct. 10, 2003
ISSN: 1527-1366
ISBN: 0-7695-2035-9
pp: 94
Mana Taghdiri , MIT CSAIL, Cambridge, MA
Ilya Shlyakhter , MIT CSAIL, Cambridge, MA
Robert Seater , MIT CSAIL, Cambridge, MA
Daniel Jackson , MIT CSAIL, Cambridge, MA
Manu Sridharan , UC Berkeley, Berkeley, CA
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.
Mana Taghdiri, Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, "Debugging Overconstrained Declarative Models Using Unsatisfiable Cores", 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), vol. 00, no. , pp. 94, 2003, doi:10.1109/ASE.2003.1240298
80 ms
(Ver 3.3 (11022016))