Abstract
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.
This research has been partially supported by MICINN Spanish project StrongSoft (TIN2012-39391-C04-04) and by the Comunidad de Madrid project N-Greens Software-CM (S2013/ICE-2731).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We have placed the sort v as the last sort in the arity to ease the presentation, but it is not required.
- 2.
We would need extra rules to take care of non-initialized registers, but this is not relevant for the technique.
- 3.
Note that we would need another rule to deal with the case where RI is not initialized, but this does not change the inference.
References
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)
Alpuente, M., Ballis, D., Frechina, F., Romero, D.: Using conditional trace slicing for improving Maude programs. Sci. Comput. Program. 80, 385–415 (2014)
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)
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)
Bethke, I., Klop, J.W., de Vrijer, R.C.: Descendants and origins in term rewriting. Inf. Comput. 159(1–2), 59–124 (2000)
Bouhoula, A., Jouannaud, J.-P., Meseguer, J.: Specification and proof in membership equational logic. Theor. Comput. Sci. 236(1–2), 35–132 (2000)
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)
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)
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)
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)
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)
Ferrara, P.: A generic static analyzer for multithreaded java programs. Softw., Pract. Exper. 43(6), 663–684 (2013)
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)
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)
Hind, M., Pioli, A.: Evaluating the effectiveness of pointer alias analyses. Sci. Comput. Program. 39(1), 31–55 (2001)
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)
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)
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)
Martí-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2), 121–154 (2002)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)
Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373(3), 213–237 (2007)
Pierce, B.C.: Types and Programming Languages. MIT Press, London (2002)
Ramalingam, G.: The undecidability of aliasing. ACM Trans. Program. Lang. Syst. 16(5), 1467–1471 (1994)
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)
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)
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)
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)
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)
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)
Acknowledgments
We thank the anonymous reviewers for their valuable comments and suggestions, which greatly improved the quality of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Riesco, A., Asavoae, I.M., Asavoae, M. (2015). Memory Policy Analysis for Semantics Specifications in Maude. In: Falaschi, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2015. Lecture Notes in Computer Science(), vol 9527. Springer, Cham. https://doi.org/10.1007/978-3-319-27436-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-27436-2_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27435-5
Online ISBN: 978-3-319-27436-2
eBook Packages: Computer ScienceComputer Science (R0)