Constraint Prioritization for Efficient Analysis of Declarative Models

The declarative modeling language Alloy and its automatic analyzer provide an effective tool-set for building designs of systems and checking their properties. The Alloy Analyzer performs bounded exhaustive analysis using offthe-shelf SAT solvers. The analyzer's performance hinges on the complexity of the models and so far, its feasibility has been shown only within limited bounds. We present a novel optimization technique that defines program slicing for declarative models and enables efficient analyses exploiting partial solutions. We present an algorithm that computes transient slices for Alloy models by partitioning them into a base and a derived slice. A satisfying solution to the base slice is systematically extended to generate a solution for the entire model, while unsatisfiability of the base implies unsatisfiability of the entire model. By generating slices, our approach enables constraint prioritization, where the base slice assumes higher priority than the derived slic...

• Type: Conference
• Year: 2008
• Where: FM
• Authors: Engin Uzuncaova, Sarfraz Khurshid
• Keywords: Alloy Analyzer, Base Slice, Enables Efficient Analyses, FM 2008, Formal Methods