Skip to main content
SpringerLink
Log in

The Rewriting Logic Semantics Project: A Progress Report

  • Conference paper
Fundamentals of Computation Theory (FCT 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6914))

Included in the following conference series:

Abstract

Rewriting logic is an executable logical framework well suited for the semantic definition of languages. Any such framework has to be judged by its effectiveness to bridge the existing gap between language definitions on the one hand, and language implementations and language analysis tools on the other. We give a progress report on how researchers in the rewriting logic semantics project are narrowing the gap between theory and practice in areas such as: modular semantic definitions of languages; scalability to real languages; support for real time; semantics of software and hardware modeling languages; and semantics-based analysis tools such as static analyzers, model checkers, and program provers.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ahrendt, W., Roth, A., Sasse, R.: Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 412–426. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Alba-Castro, M., Alpuente, M., Escobar, S.: Abstract certification of global non-interference in rewriting logic. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 105–124. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  3. Alba-Castro, M., Alpuente, M., Escobar, S.: Approximating non-interference and erasure in rewriting logic. In: Proc. SYNASC, pp. 124–132. IEEE, Los Alamitos (2010)

    Google Scholar 

  4. AlTurki, M., Dhurjati, D., Yu, D., Chander, A., Inamura, H.: Formal specification and analysis of timing properties in software systems. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 262–277. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. AlTurki, M., Meseguer, J.: Real-time rewriting semantics of Orc. In: Proc. PPDP, Poland, pp. 131–142. ACM Press, New York (2007)

    Chapter  Google Scholar 

  6. AlTurki, M., Meseguer, J.: Reduction semantics and formal analysis of Orc programs. In: Proc. Workshop on Automated Specification and Verification of Web Systems (WWV 2007). ENTCS, vol. 200(3), pp. 25–41. Elsevier, Amsterdam (2008)

    Google Scholar 

  7. AlTurki, M., Meseguer, J.: Dist-Orc: A rewriting-based distributed implementation of Orc with formal analysis. In: Proc. RTRTS 2010. Electronic Proceedings in Theoretical Computer Science, vol. 36, pp. 26–45. CoRR (2010)

    Google Scholar 

  8. Aoumeur, N.: Integrating and rapid-prototyping UML structural and behavioural diagrams using rewriting logic. In: Pidduck, A.B., Mylopoulos, J., Woo, C.C., Ozsu, M.T. (eds.) CAiSE 2002. LNCS, vol. 2348, pp. 296–310. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Bae, K., Ölveczky, P.C.: Extending the Real-Time Maude semantics of Ptolemy to hierarchical DE models. In: Proc. RTRTS 2010. Electronic Proceedings in Theoretical Computer Science, vol. 36, pp. 46–66. CoRR (2010)

    Google Scholar 

  10. Bae, K., Ölveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. Technical report, University of Illinois at Urbana-Champaign (2005), http://hdl.handle.net/2142/25091

  11. Bae, K., Ölveczky, P.C., Feng, T.H., Tripakis, S.: Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 717–736. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  12. Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96(1), 217–248 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  13. Bjørk, J., Johnsen, E.B., Owe, O., Schlatte, R.: Lightweight time modeling in timed Creol. In: Proc. RTRTS 2010. Electronic Proceedings in Theoretical Computer Science, vol. 36, pp. 67–81. CoRR (2010)

    Google Scholar 

  14. Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning 43(3), 263–288 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  15. Boronat, A.: MOMENT: A Formal Framework for MOdel ManageMENT. PhD thesis, Universitat Politècnica de València, Spain (2007)

    Google Scholar 

  16. Boronat, A., Carsí, J.A., Ramos, I.: Automatic reengineering in MDA using rewriting logic as transformation engine. In: Proc. CSMR 2005, pp. 228–231. IEEE, Los Alamitos (2005)

    Google Scholar 

  17. Boronat, A., Heckel, R., Meseguer, J.: Rewriting logic semantics and verification of model transformations. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 18–33. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  18. Boronat, A., Meseguer, J.: Algebraic semantics of OCL-constrained metamodel specifications. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol. 33, pp. 96–115. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Boronat, A., Meseguer, J.: MOMENT2: EMF model transformations in Maude. In: Vallecillo, A., Sagardui, G. (eds.) Actas de las XIV Jornadas de Ingeniería del Software y Bases de Datos, JISBD 2009, San Sebastián, España, September 8-11, pp. 178–179 (2009)

    Google Scholar 

  20. Boronat, A., Meseguer, J.: An algebraic semantics for MOF. Formal Aspects of Computing 22(3-4), 269–296 (2010)

    Article  MATH  Google Scholar 

  21. Boronat, A., Ölveczky, P.C.: Formal real-time model transformations in MOMENT2. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 29–43. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Borras, P., Clément, D., Despeyroux, T., Incerpi, J., Kahn, G., Lang, B., Pascual, V.: CENTAUR: The system. In: Software Development Environments (SDE), pp. 14–24 (1988)

    Google Scholar 

  23. Braga, C.: Rewriting Logic as a Semantic Framework for Modular Structural Operational Semantics. PhD thesis, Departamento de Informática, Pontifícia Universidade Católica do Rio de Janeiro, Brazil (2001)

    Google Scholar 

  24. Braga, C., Haeusler, E.H., Meseguer, J., Mosses, P.D.: Mapping modular SOS to rewriting logic. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 262–277. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  25. Braga, C., Meseguer, J.: Modular rewriting semantics in practice. In: Proc. WRLA 2004. ENTCS, vol. 117, pp. 393–416. Elsevier, Amsterdam (2004)

    Google Scholar 

  26. Broy, M., Wirsing, M., Pepper, P.: On the algebraic definition of programming languages. ACM TOPLAS 9(1), 54–99 (1987)

    Article  MATH  Google Scholar 

  27. Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1-3), 386–414 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  28. Chalub, F.: An implementation of Modular SOS in Maude. Master’s thesis, Universidade Federal Fluminense, Niterói, RJ, Brazil (May 2005)

    Google Scholar 

  29. Chalub, F., Braga, C.: Maude MSOS tool. Universidade Federal Fluminense, www.ic.uff.br/~frosario/2o-workshop-vas-novembro-2004.pdf

  30. Chalub, F., Braga, C.: A Modular Rewriting Semantics for CML. Journal of Universal Computer Science 10(7), 789–807 (2004)

    MathSciNet  Google Scholar 

  31. Chen, F., Roşu, G., Venkatesan, R.P.: Rule-based analysis of dimensional safety. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 197–207. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  32. Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  33. Clavel, M., Egea, M.: ITP/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 368–373. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  34. Clavel, M., Santa-Cruz, J.: ASIP + ITP: A verification tool based on algebraic semantics. In: López-Fraguas, F.J. (ed.) Actas de las V Jornadas sobre Programación y Lenguajes, PROLE 2005, Granada, España, Septiembre 14-16, pp. 149–158. Thomson (2005)

    Google Scholar 

  35. Clément, D., Despeyroux, J., Hascoet, L., Kahn, G.: Natural semantics on the computer. In: Fuchi, K., Nivat, M. (eds.) Proceedings, France-Japan AI and CS Symposium, ICOT 1986, pp. 49–89 (1986); Also, Information Processing Society of Japan, Technical Memorandum PL-86-6

    Google Scholar 

  36. d’Amorim, M., Roşu, G.: An Equational Specification for the Scheme Language. Journal of Universal Computer Science 11(7), 1327–1348 (2005); Also Technical Report No. UIUCDCS-R-2005-2567 (April 2005)

    Google Scholar 

  37. Ellison, C., Roşu, G.: A formal semantics of C with applications. Technical Report University of Illinois (November 2010), http://hdl.handle.net/2142/17414

  38. Ellison, C., Şerbănuţă, T.F., Roşu, G.: A rewriting logic approach to type inference. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 135–151. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  39. Farzan, A.: Static and dynamic formal analysis of concurrent systems and languages: a semantics-based approach. PhD thesis, University of Illinois at Urbana-Champaign (2007)

    Google Scholar 

  40. Farzan, A., Chen, F., Bevilacqua, V., 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)

    Chapter  Google Scholar 

  41. Farzan, A., Meseguer, J.: Partial order reduction for rewriting semantics of programming languages. In: Proc. WRLA 2006. ENTCS, vol. 176(4), pp. 61–78 (2007)

    Google Scholar 

  42. Farzan, A., Bevilacqua, V., 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)

    Chapter  Google Scholar 

  43. Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the λ-calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts, Denmark, pp. 193–219 (August 1986)

    Google Scholar 

  44. Fernández Alemán, J.L., Toval Álvarez, J.A.: Can intuition become rigorous? Foundations for UML model verification tools. In: Proc. ISSRE 2000, pp. 344–355. IEEE, Los Alamitos (2000)

    Google Scholar 

  45. Friedman, D.P., Wand, M., Haynes, C.T.: Essentials of Programming Languages, 2nd edn. MIT Press, Cambridge (2001)

    MATH  Google Scholar 

  46. Garrido, A., Meseguer, J., Johnson, R.: Algebraic semantics of the C preprocessor and correctness of its refactorings. Technical Report UIUCDCS-R-2006-2688, CS Dept., University of Illinois at Urbana-Champaign (February 2006)

    Google Scholar 

  47. Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)

    MATH  Google Scholar 

  48. Goguen, J., Meseguer, J.: Security policies and security models. In: Proceedings of the 1982 Symposium on Security and Privacy, pp. 11–20. IEEE, Los Alamitos (1982)

    Google Scholar 

  49. Goguen, J.A., Parsaye-Ghomi, K.: Algebraic denotational semantics using parameterized abstract modules. In: Díaz, J., Ramos, I. (eds.) Formalization of Programming Concepts. LNCS, vol. 107, pp. 292–309. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  50. Gurevich, Y.: Evolving algebras 1993: Lipari Guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–37. Oxford University Press, Oxford (1994)

    Google Scholar 

  51. Gurevich, Y., Huggins, J.K.: The semantics of the C programming language. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 274–308. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  52. Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  53. Hills, M., Chen, F., Roşu, G.: Pluggable Policies for C. Technical Report UIUCDCS-R-2008-2931, University of Illinois at Urbana-Champaign (2008)

    Google Scholar 

  54. Hills, M., Şerbănuţă, T.F., Roşu, G.: A rewrite framework for language definitions and for generation of efficient interpreters. In: Proc. of WRLA 2006. ENTCS, vol. 176(4), pp. 215–231. Elsevier, Amsterdam (2007)

    Google Scholar 

  55. Johnsen, E.B., Owe, O., Axelsen, E.W.: A runtime environment for concurrent objects with asynchronous method calls. In: Proc. WRLA 2004. ENTCS, vol. 117, Elsevier, Amsterdam (2004)

    Google Scholar 

  56. Kahn, G.: Natural semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)

    Google Scholar 

  57. Katelman, M., Keller, S., Meseguer, J.: Concurrent rewriting semantics and analysis of asynchronous digital circuits. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 140–156. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  58. Katelman, M., Meseguer, J.: A rewriting semantics for ABEL with applications to hardware/software co-design and analysis. In: Proc. WRLA 2006. ENTCS, vol. 176(4), pp. 47–60. Elsevier, Amsterdam (2007)

    Google Scholar 

  59. Katelman, M., Meseguer, J.: vlogmt: A strategy language for simulation-based verification of hardware. In: Raz, O. (ed.) HVC 2010. LNCS, vol. 6504, pp. 129–145. Springer, Heidelberg (2010)

    Google Scholar 

  60. Katelman, M., Meseguer, J., Escobar, S.: Directed-logical testing for functional verification of microprocessors. In: MEMOCODE 2008, pp. 89–100. IEEE, Los Alamitos (2008)

    Google Scholar 

  61. Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, Dordrecht (2000)

    Google Scholar 

  62. Knapp, A.: Generating rewrite theories from UML collaborations. In: Futatsugi, K., Nakagawa, A.T., Tamai, T. (eds.) Cafe: An Industrial-Strength Algebraic Formal Method, pp. 97–120. Elsevier, Amsterdam (2000)

    Chapter  Google Scholar 

  63. Knapp, A.: A Formal Approach to Object-Oriented Software Engineering. Shaker Verlag, Aachen, Germany, 2001. PhD thesis, Institut für Informatik, Universität München (2000)

    Google Scholar 

  64. Lee, E.A.: Modeling concurrent real-time processes using discrete events. Ann. Software Eng. 7, 25–45 (1999)

    Article  Google Scholar 

  65. Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Proc. POPL 1995, pp. 333–343. ACM Press, New York (1995)

    Google Scholar 

  66. Martí-Oliet, N., Meseguer, J.: Rewriting logic as a logical and semantic framework. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, 2nd edn., vol. 9, pp. 1–87. Kluwer, Dordrecht (2002)

    Chapter  Google Scholar 

  67. Meredith, P., Hills, M., Roşu, G.: A K definition of Scheme. Technical Report UIUCDCS-R-2007-2907, Department of Computer Science, University of Illinois at Urbana-Champaign (2007)

    Google Scholar 

  68. Meredith, P., Katelman, M., Meseguer, J., Roşu, G.: A formal executable semantics of Verilog. In: Proc. MEMOCODE 2010, pp. 179–188. IEEE, Los Alamitos (2010)

    Google Scholar 

  69. Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  70. Meseguer, J.: Rewriting logic as a semantic framework for concurrency: a progress report. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 331–372. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  71. 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)

    Chapter  Google Scholar 

  72. Meseguer, J.: Software specification and verification in rewriting logic. In: Broy, M., Pizka, M. (eds.) Models, Algebras, and Logic of Engineering Software, NATO Advanced Study Institute, Marktoberdorf, Germany, July 30 – August 11, pp. 133–193. IOS Press, Amsterdam (2002)

    Google Scholar 

  73. Meseguer, J., Braga, C.: Modular rewriting semantics of programming languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 364–378. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  74. Meseguer, J., Futatsugi, K., Winkler, T.: Using rewriting logic to specify, program, integrate, and reuse open concurrent systems of cooperating agents. In: Proceedings of the 1992 International Symposium on New Models for Software Architecture, Tokyo, Japan, pp. 61–106. Research Institute of Software Engineering (November 1992)

    Google Scholar 

  75. Meseguer, J., Ölveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 303–320. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  76. Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoretical Computer Science 373, 213–237 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  77. Bevilacqua, V., 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)

    Chapter  Google Scholar 

  78. Miller, D.: Representing and reasoning with operational semantics. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 4–20. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  79. Misra, J.: Computation orchestration: A basis for wide-area computing. In: Broy, M. (ed.) Proc. of the NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems Marktoberdorf, Germany. NATO ASI Series (2004)

    Google Scholar 

  80. Misra, J., Cook, W.R.: Computation orchestration. Software and System Modeling 6(1), 83–110 (2007)

    Article  Google Scholar 

  81. Moggi, E.: An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Edinburgh University, Dept. of Computer Science (June 1989)

    Google Scholar 

  82. Mokhati, F., Badri, M.: Generating Maude specifications from UML use case diagrams. Journal of Object Technology 8(2), 319–136 (2009)

    Google Scholar 

  83. Mokhati, F., Gagnon, P., Badri, M.: Verifying UML diagrams with model checking: A rewriting logic based approach. In: Proc. QSIC 2007, pp. 356–362. IEEE, Los Alamitos (2007)

    Google Scholar 

  84. Mokhati, F., Sahraoui, B., Bouzaher, S., Kimour, M.T.: A tool for specifying and validating agents’ interaction protocols: From Agent UML to Maude. Journal of Object Technology 9(3), 59–77 (2010)

    Article  Google Scholar 

  85. Mosses, P.D.: Unified algebras and action semantics. In: Cori, R., Monien, B. (eds.) STACS 1989. LNCS, vol. 349, pp. 17–35. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  86. Mosses, P.D.: Denotational semantics. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, ch. 11, North-Holland, Amsterdam (1990)

    Google Scholar 

  87. Mosses, P.D.: Modular structural operational semantics. J. Log. Algebr. Program. 60-61, 195–228 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  88. Nadathur, G., Miller, D.: An overview of λProlog. In: Bowen, K., Kowalski, R. (eds.) Fifth Int. Joint Conf. and Symp. on Logic Programming, pp. 810–827. The MIT Press, Cambridge (1988)

    Google Scholar 

  89. Nakajima, S.: Using algebraic specification techniques in development of object-oriented frameworks. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1664–1683. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  90. Nakajima, S., Futatsugi, K.: An object-oriented modeling method for algebraic specifications in CafeOBJ. In: Proc. ICSE 1997. ACM, New York (1997)

    Google Scholar 

  91. Norrish, M.: C formalised in HOL. Technical Report UCAM-CL-TR-453, University of Cambridge (December 1998)

    Google Scholar 

  92. Ölveczky, P.C., Boronat, A., Meseguer, J.: Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010. LNCS, vol. 6117, pp. 47–62. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  93. Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285(2), 359–405 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  94. Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)

    Article  MATH  Google Scholar 

  95. Papaspyrou, N.S.: A Formal Semantics for the C Programming Language. PhD thesis, National Technical University of Athens (February 1998)

    Google Scholar 

  96. Papaspyrou, N.S.: Denotational semantics of ANSI C. Computer Standards and Interfaces 23(3), 169–185 (2001)

    Article  Google Scholar 

  97. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proc. PLDI 1988, pp. 199–208. ACM Press, New York (1988)

    Google Scholar 

  98. Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  99. Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61, 17–139 (2004); Previously published as technical report DAIMI FN-19, Aarhus University (1981)

    Article  MathSciNet  MATH  Google Scholar 

  100. Rivera, J.E., Durán, F., Vallecillo, A.: On the behavioral semantics of real-time domain specific visual languages. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 174–190. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  101. Roşu, G.: CS322, Fall, - Programming Language Design: Lecture Notes. Technical Report UIUCDCS-R-2003-2897, University of Illinois at Urbana-Champaign, Dept. of Computer Science, Notes of a course taught at UIUC (2003)

    Google Scholar 

  102. Roşu, G., Ştefănescu, A.: Matching logic: A new program verification approach (nier track). In: Proc. ICSE 2011(2011)

    Google Scholar 

  103. Roşu, G., Ellison, C., Schulte, W.: Matching logic: An alternative to hoare/Floyd logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 142–162. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  104. Roşu, G., Venkatesan, R.P., Whittle, J., Leuştean, L.: Certifying optimality of state estimation programs. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 301–314. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  105. Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  106. Sasse, R.: Taclets vs. rewriting logic – relating semantics of Java. Master’s thesis, Fakultät für Informatik, Universität Karlsruhe, Germany, Technical Report in Computing Science No. 2005-16 (May 2005)

    Google Scholar 

  107. Sasse, R., Meseguer, J.: Java+ITP: A verification tool based on hoare logic and algebraic semantics. In: Proc. WRLA 2006. ENTCS, vol. 176(4), pp. 29–46 (2007)

    Google Scholar 

  108. Schmidt, D.A.: Denotational Semantics – A Methodology for Language Development. Allyn and Bacon, Boston (1986)

    Google Scholar 

  109. Scott, D.: Outline of a mathematical theory of computation. In: Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems, pp. 169–176. Princeton University, Princeton (1970); Also appeared as Technical Monograph PRG 2, Oxford University, Programming Research Group

    Google Scholar 

  110. Scott, D., Strachey, C.: Toward a mathematical semantics for computer languages. In: Proc. Symp. on Computers and Automata. Microwave Research Institute Symposia Series, vol. 21, Polytechnical Institute of Brooklyn (1971)

    Google Scholar 

  111. T. F. Şerbănuţă. A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD thesis, Department of Computer Science, University of Illinois at Urbana-Champaign (2010)

    Google Scholar 

  112. Şerbănuţă, T.F., Roşu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Information and Computation 207(2), 305–340 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  113. Slonneger, K., Kurtz, B.L.: Formal Syntax and Semantics of Programming Languages. Addison-Wesley, Reading (1995)

    MATH  Google Scholar 

  114. Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001)

    Book  MATH  Google Scholar 

  115. Stehr, M.-O., Talcott, C.: PLAN in Maude: Specifying an active network programming language. In: Proc. WRLA 2002. ENTCS, vol. 117, Elsevier, Amsterdam (2002)

    Google Scholar 

  116. Stehr, M.-O., Talcott, C.L.: Practical techniques for language design and prototyping. In: Dagstuhl Seminar 05081 on Foundations of Global Computing, February 20 – 25, Schloss Dagstuhl, Wadern (2005)

    Google Scholar 

  117. Thati, P., Sen, K., Martí-Oliet, N.: An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0. In: Proc. WRLA 2002. ENTCS, Elsevier, Amsterdam (2002)

    Google Scholar 

  118. van Deursen, A., Heering, J., Klint, P.: Language Prototyping: An Algebraic Specification Approach. World Scientific, Singapore (1996)

    Book  MATH  Google Scholar 

  119. Verdejo, A.: Maude como marco semántico ejecutable. PhD thesis, Facultad de Informática, Universidad Complutense, Madrid, Spain (2003)

    Google Scholar 

  120. Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude 2. In: Proc. WRLA 2002. ENTCS, Elsevier, Amsterdam (2002)

    Google Scholar 

  121. Verdejo, A., Martí-Oliet, N.: Two case studies of semantics execution in Maude: CCS and LOTOS. Formal Methods in System Design 27(1-2), 113–172 (2005)

    Article  MATH  Google Scholar 

  122. Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. Journal of Logic and Algebraic Programming 67(1-2), 226–293 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  123. Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  124. Wadler, P.: The essence of functional programming. In: Proc. POPL 1992, pp. 1–14. ACM Press, New York (1992)

    Google Scholar 

  125. Wand, M.: First-order identities as a defining language. Acta Informatica 14, 337–357 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  126. Wehrman, I., Kitchin, D., Cook, W.R., Misra, J.: A timed semantics of Orc. Theor. Comput. Sci. 402(2-3), 234–248 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  127. Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. In: Proc. WRLA 1996. ENTCS, vol. 4, pp. 322–360 (1996)

    Google Scholar 

  128. Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. Theoretical Computer Science 285(2), 519–560 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  129. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois, Urbana-Champaign, USA

    José Meseguer & Grigore Roşu

Authors
  1. José Meseguer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Grigore Roşu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics, University of Oslo, Postboks 1080 Blindern, 0316, Oslo, Norway

    Olaf Owe  & Martin Steffen  & 

  2. Department of Informatics, University of Bergen, Postboks 7800, 5020, Bergen, Norway

    Jan Arne Telle

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Meseguer, J., Roşu, G. (2011). The Rewriting Logic Semantics Project: A Progress Report. In: Owe, O., Steffen, M., Telle, J.A. (eds) Fundamentals of Computation Theory. FCT 2011. Lecture Notes in Computer Science, vol 6914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22953-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22953-4_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22952-7

  • Online ISBN: 978-3-642-22953-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation