loading...
Kato: A Program Slicing Tool for Declarative Specifications
Minneapolis, Minnesota May 20-May 26
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICSE.2007.4729th International Conference on Soft ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Engin Uzuncaova, The University of Texas at Austin, USA
Sarfraz Khurshid, The University of Texas at Austin, USA
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.
Citation:
Engin Uzuncaova, Sarfraz Khurshid, "Kato: A Program Slicing Tool for Declarative Specifications," icse, pp.767-770, 29th International Conference on Software Engineering (ICSE'07), 2007
Usage of this product signifies your acceptance of the Terms of Use.