Declarative specifications exhibit a variety of problems, such as inadvertently overconstrained axioms and underconstrained conjectures, that are hard to diagnose with model checking and theorem proving alone. Recycling core extraction is a new coverage analysis that pinpoints an irreducible unsatisfiable core of a declarative specification. It is based on resolution refutation proofs generated by resolution engines, such as SAT solvers and resolution theorem provers. The extraction algorithm is described, and proved correct, for a generalized specification language with a regular translation to the input logic of a resolution engine. It has been implemented for the Alloy language and evaluated on a variety of specifications, with promising results. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Torlak, E., Chang, F. S. H., & Jackson, D. (2008). Finding minimal unsatisfiable cores of declarative specifications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5014 LNCS, pp. 326–341). https://doi.org/10.1007/978-3-540-68237-0_23
Mendeley helps you to discover research relevant for your work.