Inspecting Rewriting Logic Computations (in a Parametric and Stepwise Way)

  • María Alpuente
  • Demis Ballis
  • Francisco Frechina
  • Julia Sapiña
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


Trace inspection is concerned with techniques that allow the trace content to be searched for specific components. This paper presents a rich and highly dynamic, parameterized technique for the trace inspection of Rewriting Logic theories that allows the non-deterministic execution of a given unconditional rewrite theory to be followed up in different ways. Using this technique, an analyst can browse, slice, filter, or search the traces as they come to life during the program execution. Starting from a selected state in the computation tree, the navigation of the trace is driven by a user-defined, inspection criterion that specifies the required exploration mode. By selecting different inspection criteria, one can automatically derive a family of practical algorithms such as program steppers and more sophisticated dynamic trace slicers that facilitate the dynamic detection of control and data dependencies across the computation tree. Our methodology, which is implemented in the Anima graphical tool, allows users to capture the impact of a given criterion thereby facilitating the detection of improper program behaviors.


Computation Tree Execution Trace Initial Term Rewrite Theory Partial Stepper 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alpuente, M., Ballis, D., Baggi, M., Falaschi, M.: A Fold/Unfold Transformation Framework for Rewrite Theories extended to CCT. In: Proc. PEPM 2010, pp. 43–52. ACM (2010)Google Scholar
  2. 2.
    Alpuente, M., Ballis, D., Espert, J., Romero, D.: Model-checking Web Applications with Web-TLR. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 341–346. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Alpuente, M., Ballis, D., Espert, J., Romero, D.: Backward Trace Slicing for Rewriting Logic Theories. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 34–48. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  4. 4.
    Alpuente, M., Ballis, D., Frechina, F., Sapiña, J.: Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJulienne. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 121–124. Springer, Heidelberg (2013)Google Scholar
  5. 5.
    Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Using Conditional Trace Slicing for improving Maude programs. Science of Computer Programming (2013) (to appear)Google Scholar
  6. 6.
    Alpuente, M., Ballis, D., Romero, D.: A Rewriting Logic Approach to the Formal Specification and Verification of Web applications. Science of Computer Programming (2013) (to appear)Google Scholar
  7. 7.
    Baggi, M., Ballis, D., Falaschi, M.: Quantitative Pathway Logic for Computational Biology. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 68–82. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Bruni, R., Meseguer, J.: Semantic Foundations for Generalized Rewrite Theories. Theoretical Computer Science 360(1-3), 386–414 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.6). Technical report, SRI Int’l Computer Science Laboratory (2011),
  10. 10.
    Clements, J., Flatt, M., Felleisen, M.: Modeling an Algebraic Stepper. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 320–334. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Durán, F., Meseguer, J.: A Maude Coherence Checker Tool for Conditional Order-Sorted Rewrite Theories. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  12. 12.
    Eker, S.: Associative-Commutative Matching via Bipartite Graph Matching. The Computer Journal 38(5), 381–399 (1995)CrossRefGoogle Scholar
  13. 13.
    Eker, S.: Associative-Commutative Rewriting on Large Terms. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 14–29. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Klop, J.W.: Term Rewriting Systems. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol. I, pp. 1–112. Oxford University Press (1992)Google Scholar
  15. 15.
    Martí-Oliet, N., Meseguer, J.: Rewriting Logic: Roadmap and Bibliography. Theoretical Computer Science 285(2), 121–154 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Meseguer, J.: Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science 96(1), 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Meseguer, J.: The Temporal Logic of Rewriting: A Gentle Introduction. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Montanari Festschrift. LNCS, vol. 5065, pp. 354–382. Springer, Heidelberg (2008)Google Scholar
  18. 18.
    Plotkin, G.D.: The Origins of Structural Operational Semantics. The Journal of Logic and Algebraic Programming 60-61(1), 3–15 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Riesco, A., Verdejo, A., Caballero, R., Martí-Oliet, N.: Declarative Debugging of Rewriting Logic Specifications. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 308–325. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  20. 20.
    Riesco, A., Verdejo, A., Martí-Oliet, N.: Declarative Debugging of Missing Answers for Maude. In: Proc. RTA 2010. LIPIcs, vol. 6, pp. 277–294 (2010)Google Scholar
  21. 21.
    TeReSe. Term Rewriting Systems. Cambridge University Press (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • María Alpuente
    • 1
  • Demis Ballis
    • 2
  • Francisco Frechina
    • 1
  • Julia Sapiña
    • 1
  1. 1.DSIC-ELPUniversitat Politècnica de ValènciaApdoSpain
  2. 2.CLIP LabTechnical University of MadridBoadilla del MonteSpain

Personalised recommendations