Memory Policy Analysis for Semantics Specifications in Maude

  • Adrián Riesco
  • Irina Mariuca Asavoae
  • Mihail AsavoaeEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


In this paper we propose an approach to the analysis of formal language semantics. In our analysis we target memory policies, namely, whether the formal specification under consideration follows a particular standard when defining how the language constructs work with the memory. More specifically, we consider Maude specifications of formal programming language semantics and we investigate these specifications at the meta-level in order to identify the memory elements (e.g., variables and values) and how the language syntactic constructs employ the memory and its elements. The current work is motivated by previous work on generic slicing in Maude, in the pursuit of making our generic slicing as general as possible. In this way, we integrate the current technique into an existing implementation of a generic semantics-based program slicer.


Formal semantics Maude Slicing Analysis Memory policies 



We thank the anonymous reviewers for their valuable comments and suggestions, which greatly improved the quality of the paper.


  1. 1.
    Albert, E., Genaim, S., Gómez-Zamalloa, M.: Live heap space analysis for languages with garbage collection. In: Proceedings of the International Symposium on Memory Management, ISMM 2009, pp. 129–138. ACM (2009)Google Scholar
  2. 2.
    Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Using conditional trace slicing for improving Maude programs. Sci. Comput. Program. 80, 385–415 (2014)CrossRefGoogle Scholar
  3. 3.
    Asavoae, I.M., Asavoae, M., Riesco, A.: Towards a formal semantics-based technique for interprocedural slicing. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 291–306. Springer, Heidelberg (2014) Google Scholar
  4. 4.
    Baufreton, P., Heckmann, R.: Reliable and precise WCET and stack size determination for a real-life embedded application. In: ISoLA 2007, Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Revue des Nouvelles Technologies de l’Information, pp. 41–48. (2007)Google Scholar
  5. 5.
    Bethke, I., Klop, J.W., de Vrijer, R.C.: Descendants and origins in term rewriting. Inf. Comput. 159(1–2), 59–124 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236(1–2), 35–132 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007) zbMATHGoogle Scholar
  8. 8.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Symposium on Principles of Programming Languages, POPL 1977, pp. 238–252. ACM (1977)Google Scholar
  9. 9.
    Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the Symposium on Principles of Programming Languages, POPL 2012, pp. 533–544. ACM (2012)Google Scholar
  10. 10.
    Farzan, A., Chen, F., Meseguer, J., Rosu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 501–505. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  11. 11.
    Farzan, A., Meseguer, J., Rosu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 132–147. Springer, Heidelberg (2004) CrossRefGoogle Scholar
  12. 12.
    Ferrara, P.: A generic static analyzer for multithreaded java programs. Softw., Pract. Exper. 43(6), 663–684 (2013)CrossRefGoogle Scholar
  13. 13.
    Field, J., Tip, F.: Dynamic dependence in term rewriting systems and its application to program slicing. Inf. Softw. Technol. 40(11–12), 609–636 (1998)CrossRefGoogle Scholar
  14. 14.
    Hills, M., Rosu, G.: A rewriting logic semantics approach to modular program analysis. In: Proceedings of the International Conference on Rewriting Techniques and Applications, RTA 2010, LIPIcs, vol. 6, pp. 151–160. (2010)Google Scholar
  15. 15.
    Hind, M., Pioli, A.: Evaluating the effectiveness of pointer alias analyses. Sci. Comput. Program. 39(1), 31–55 (2001)CrossRefzbMATHGoogle Scholar
  16. 16.
    Huet, G.P., Lévy, J.: Computations in orthogonal rewriting systems, I. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 395–414. (1991)Google Scholar
  17. 17.
    Klop, J.W.: Term rewriting systems from Church-Rosser to Knuth-Bendix and beyond. In: Paterson, M.S. (ed.) Automata, Languages and Programming. LNCS, vol. 443, pp. 350–369. Springer, Heidelberg (1990) CrossRefGoogle Scholar
  18. 18.
    Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1–31 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2), 121–154 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373(3), 213–237 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Pierce, B.C.: Types and Programming Languages. MIT Press, London (2002) zbMATHGoogle Scholar
  23. 23.
    Ramalingam, G.: The undecidability of aliasing. ACM Trans. Program. Lang. Syst. 16(5), 1467–1471 (1994)CrossRefGoogle Scholar
  24. 24.
    Regehr, J., Reid, A., Webb, K.: Eliminating stack overflow by abstract interpretation. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 306–322. Springer, Heidelberg (2003) CrossRefGoogle Scholar
  25. 25.
    Riesco, A.: Using semantics specified in maude to generate test cases. In: Roychoudhury, A., D’Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 90–104. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  26. 26.
    Riesco, A., Asavoae, I.M., Asavoae, M.: A generic program slicing technique based on language definitions. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 248–264. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  27. 27.
    Rosu, G., Stefanescu, A.: Matching logic: a new program verification approach. In: Proceedings of the International Conference on Software Engineering, ICSE 2011, pp. 868–871. ACM (2011)Google Scholar
  28. 28.
    Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-cc multiprocessor machine code. In: Proceedings of the Symposium on Principles of Programming Languages, POPL 2009, pp. 379–391. ACM (2009)Google Scholar
  29. 29.
    Venkitaraman, R., Gupta, G.: Static program analysis of embedded executable assembly code. In: Proceedings of the International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, CASES 2004, pp. 157–166. ACM (2004)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Adrián Riesco
    • 1
  • Irina Mariuca Asavoae
    • 2
  • Mihail Asavoae
    • 3
    Email author
  1. 1.Universidad Complutense de MadridMadridSpain
  2. 2.Swansea UniversitySwanseaUK
  3. 3.Inria Paris-RocquencourtParisFrance

Personalised recommendations