Finding Minimal Unsatisfiable Cores of Declarative Specifications

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.

• Type: Conference
• Year: 2008
• Where: FM
• Authors: Emina Torlak, Felix Sheng-Ho Chang, Daniel Jackson
• Keywords: Declarative Specification, FM 2008, Formal Methods, Resolution Engine, Resolution Theorem Provers