Abstract
The technologies developed to solve the verifying compiler grand challenge should be generic, that is, not tied to a particular language but widely applicable to many languages. Such technologies should also be semantics-based, that is, based on a rigorous formal semantics of the languages.
For this, a computational logical framework with efficient executability and a spectrum of meta-tools can serve as a basis on which to: (1) define the formal semantics of any programming language; and (2) develop generic program analysis techniques and tools that can be instantiated to generate powerful analysis tools for each language of interest.
Not all logical frameworks can serve such purposes well. We first list some specific requirements that we think are important to properly address the grand challenge. Then we present our experience with rewriting logic as supported by the Maude system and its formal tool environment. Finally, we discuss some future directions of research.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Borovanský, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science 285, 155–185 (2002)
Braga, C., Meseguer, J.: Modular rewriting semantics in practice. In: Proc. WRLA 2004, ENTCS
Cervesato, I., Stehr, M.-O.: Representing the msr cryptoprotocol specification language in an extension of rewriting logic with dependent types. In: Degano, P. (ed.) Proc. Fifth International Workshop on Rewriting Logic and its Applications (WRLA 2004), Barcelona, Spain, March 27 - 28, 2004, Elsevier ENTCS, Amsterdam (2004)
Chalub, F., Braga, C.: A Modular Rewriting Semantics for CML. Journal of Universal Computer Science 10(7), 789–807 (2004), http://www.jucs.org/jucs_10_7/a_modular_rewriting_semantics
Clavel, M.: Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications. In: CSLI Publications (2000)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (June 2003), http://maude.cs.uiuc.edu
Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Algebraic Formal Method, Elsevier, Amsterdam (2000), http://maude.cs.uiuc.edu
Clavel, M., Palomino, M.: The ITP tool’s manual. Universidad Complutense, Madrid (April 2005), http://maude.sip.ucm.es/itp/
d’Amorim, M., Roşu, G.: An Equational Specification for the Scheme Language. In: Proceedings of the 9th Brazilian Symposium on Programming Languages (SBLP 2005), 2005. Also Technical Report No. UIUCDCS-R-2005-2567 (April 2005) (to appear)
Durán, F.: A reflective module algebra with applications to the Maude language. Ph.D. Thesis, University of Málaga (1999)
Durán, F.: Coherence checker and completion tools for Maude specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
Durán, F.: Termination checker and Knuth-Bendix completion tools for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
Durán, F., Lucas, S., Meseguer, J., Marché, C., Urbain, X.: Proving termination of membership equational programs. In: Sestoft, P., Heintze, N. (eds.) Proc. of ACM SIGPLAN 2004 Symposium on Partial Evaluation and Program Manipulation, PEPM 2004, pp. 147–158. ACM Press, New York (2004)
Durán, F., Meseguer, J.: A Church-Rosser checker tool for Maude equational specifications. Manuscript, Computer Science Laboratory, SRI International (2000), http://maude.cs.uiuc.edu/papers
Durán, F., Meseguer, J.: On parameterized theories and views in Full Maude 2.0. In: Futatsugi, K. (ed.) Futatsugi, editor, Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2000)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications, ENTCS, Elsevier, Amsterdam (2002)
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 230–234. Springer, Heidelberg (2003)
Farzan, A., Cheng, F., Meseguer, J., Roşu, 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.: Partial order reduction for rewriting semantics of programming languages, Manuscript, submitted for publication (2005)
Farzan, A., Meseguer, J., Roşu, 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)
Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, AMAST Series (1998)
Hendrix, J., Meseguer, J., Clavel, M.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)
Holzmann, G.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2003)
Johnsen, E.B., Owe, O., Axelsen, E.W.: A runtime environment for concurrent objects with asynchronous method calls. In: Martí-Oliet, N. (ed.) Proc. 5th. Intl. Workshop on Rewriting Logic and its Applications, ENTCS, Elsevier, Amsterdam (2004)
Lowry, M., Pressburger, T., Roşu, G.: Certifying domain-specific policies. In: Proceedings, International Conference on Automated Software Engineering (ASE 2001), pp. 81–90. IEEE, Los Alamitos, San Diego, California (2001)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Meseguer, J., Roşu, G.: Rewriting logic semantics: From language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 1–44. Springer, Heidelberg (2004)
Meseguer, J., Roşu, G.: Rewriting logic semantics: From language specifications to formal analysis tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 1–44. Springer, Heidelberg (2004)
Meseguer, J., Roşu, G.: The rewriting logic semantics project. In: Proc. of SOS 2005, ENTCS, Elsevier, Amsterdam (to appear, 2005)
Mosses, P.D.: Foundations of modular SOS. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 70–80. Springer, Heidelberg (1999)
Ölveczky, P.C., Meseguer, J.: Real-Time Maude 2.1. In: Martí-Oliet, N. (ed.) Proc. 5th Intl. Workshop on Rewriting Logic and its Applications, ENTCS, Elsevier, Amsterdam (2004)
Palomino, M.: A predicate abstraction tool for Maude. Documentation and tool, http://maude.sip.ucm.es/~miguelpt/bibliography.html
Park, D.Y.W., Stern, U., Skakkebæk, J.U., Dill, D.L.: Java model checking. In: ASE 2001, pp. 253–256 (2000)
Roşu, G.: Programming language classes. Department of Computer Science, University of Illinois at Urbana-Champaign, http://fsl.cs.uiuc.edu/~grosu/classes/
Roşu, G., Chen, F.: Certifying measurement unit safety policy. In: Automated Software Engineering, 2003. Proc. 18th IEEE Intl. Conference, pp. 304–309 (2003)
Stehr, M.-O., Cervesato, I., Reich, S.: An execution environment for the MSR cryptoprotocol specification language, http://formal.cs.uiuc.edu/stehr/msr.html
Stehr, M.-O., Talcott, C.: PLAN in Maude: Specifying an active network programming language. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications, ENTCS, Elsevier, Amsterdam (2002)
Stehr, M.-O., Talcott, C.L.: Practical techniques for language design and prototyping. In: Fiadeiro, J.L., Montanari, U., Wirsing, M. (eds.) Abstracts Collection of the Dagstuhl Seminar 05081 on Foundations of Global Computing. 2005, Schloss Dagstuhl, Wadern, Germany (February 20–25, 2005)
Thati, P., Sen, K., Martí-Oliet, N.: An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications, ENTCS, Elsevier, Amsterdam (2002)
Verdejo, A.: Maude como marco semántico ejecutable. PhD thesis, Facultad de Informática, Universidad Complutense, Madrid, Spain (2003)
Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude. In: In Proc. FORTE/PSTV 2000, vol. 183, pp. 351–366 (2000)
Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude 2. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications, ENTCS, Elsevier, Amsterdam (2002)
Visser, W., Havelund, K., Brat, G., Park, S.: Java PathFinder - second generation of a Java model checker. In: Proceedings of Post-CAV Workshop on Advances in Verification (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Meseguer, J., Roşu, G. (2008). Computational Logical Frameworks and Generic Program Analysis Technologies. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)