Slicing from Formal Semantics: Chisel

  • Adrián RiescoEmail author
  • Irina Măriuca Asăvoae
  • Mihail Asăvoae
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10202)


We describe Chisel—a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics. This semantics is assumed to be a rewriting logic specification, given in Maude, while the program is a ground term of this specification. We present the tool on two types of language paradigms: high-level, imperative and low-level assembly languages. We conduct experiments with standard benchmarking used in avionics.


  1. 1.
    Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Combining runtime checking and slicing to improve Maude error diagnosis. In: Martí-Oliet, N., Ölveczky, P.C., Talcott, C. (eds.) Logic, Rewriting, and Concurrency. LNCS, vol. 9200, pp. 72–96. Springer, Cham (2015). doi: 10.1007/978-3-319-23165-5_3 CrossRefGoogle Scholar
  2. 2.
    Binkley, D., Gold, N., Harman, M., Islam, S., Krinke, J., Yoo, S.: ORBS: language-independent program slicing. In: SIGSOFT FSE 2014, pp. 109–120. ACM (2014)Google Scholar
  3. 3.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71999-1 zbMATHGoogle Scholar
  4. 4.
    Danicic, S., Harman, M.: Espresso: a slicer generator. In: SAC 2000, pp. 831–839. ACM (2000)Google Scholar
  5. 5.
    Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoret. Comput. Sci. 373(3), 213–237 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Nemer, F., Cassé, H., Sainrat, P., Bahsoun, J.P., Michiel, M.D.: PapaBench: a free real-time benchmark. In: WCET 2006. IBFI, Schloss Dagstuhl (2006)Google Scholar
  7. 7.
    Riesco, A., Asavoae, I.M., Asavoae, M.: Memory policy analysis for semantics specifications in Maude. In: Falaschi, M. (ed.) LOPSTR 2015. LNCS, vol. 9527, pp. 293–310. Springer, Cham (2015). doi: 10.1007/978-3-319-27436-2_18 CrossRefGoogle Scholar
  8. 8.
    Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397–434 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Tip, F.: A survey of program slicing techniques. JPL 3(3), 121–189 (1995)Google Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  • Adrián Riesco
    • 1
    Email author
  • Irina Măriuca Asăvoae
    • 2
  • Mihail Asăvoae
    • 2
  1. 1.Universidad Complutense de MadridMadridSpain
  2. 2.Inria ParisParisFrance

Personalised recommendations