Kato: A Program Slicing Tool for Declarative Specifications

This paper presents Kato, a tool that implements a novel class of optimizations that are inspired by program slicing for imperative languages but are applicable to analyzable declarative languages, such as Alloy. Kato implements a novel algorithm for slicing declarative models written in Alloy and leverages its relational engine KodKod for analysis. Given an Alloy model, Kato identifies a slice representing the model's core: a satisfying instance for the core can systematically be extended into a satisfying instance for the entire model, while unsatisfiability of the core implies unsatisfiability of the entire model. The experimental results show that for a variety of subject models Kato's slicing algorithm enables an order of magnitude speed-up over Alloy's default translation to SAT.

• Type: Conference
• Year: 2007
• Where: ICSE
• Authors: Engin Uzuncaova, Sarfraz Khurshid
• Keywords: Alloy Model, ICSE 2007, Paper Presents Kato, Software Engineering, Subject Models Kato