Sciweavers

Share
ICSE
2007
IEEE-ACM

Kato: A Program Slicing Tool for Declarative Specifications

11 years 12 months ago
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.
Engin Uzuncaova, Sarfraz Khurshid
Added 09 Dec 2009
Updated 09 Dec 2009
Type Conference
Year 2007
Where ICSE
Authors Engin Uzuncaova, Sarfraz Khurshid
Comments (0)
books