loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
29th International Conference on Software Engineering (ICSE'07)
Kato: A Program Slicing Tool for Declarative Specifications
Minneapolis, Minnesota
May 20-May 26
ISBN: 0-7695-2828-7
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.