×

The rewriting logic semantics project: a progress report. (English) Zbl 1342.68198

Owe, Olaf (ed.) et al., Fundamentals of computation theory. 18th international symposium, FCT 2011, Oslo, Norway, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22952-7/pbk). Lecture Notes in Computer Science 6914, 1-37 (2011).
Summary: 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.
For the entire collection see [Zbl 1220.68019].

MSC:

68Q55 Semantics in the theory of computing
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

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) · Zbl 1143.68348 · doi:10.1007/11591191_29
[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) · Zbl 1312.68049 · doi:10.1007/978-3-642-17071-3_6
[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) · Zbl 1312.68049
[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) · Zbl 05535537 · doi:10.1007/978-3-642-00593-0_18
[5] AlTurki, M., Meseguer, J.: Real-time rewriting semantics of Orc. In: Proc. PPDP, Poland, pp. 131–142. ACM Press, New York (2007) · doi:10.1145/1273920.1273938
[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)
[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) · doi:10.4204/EPTCS.36.2
[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) · Zbl 1046.68663 · doi:10.1007/3-540-47961-9_22
[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) · doi:10.4204/EPTCS.36.3
[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) · Zbl 05635837 · doi:10.1007/978-3-642-10373-5_37
[12] Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96(1), 217–248 (1992) · Zbl 0747.68013 · doi:10.1016/0304-3975(92)90185-I
[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) · doi:10.4204/EPTCS.36.4
[14] Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning 43(3), 263–288 (2009) · Zbl 1185.68136 · doi:10.1007/s10817-009-9148-3
[15] Boronat, A.: MOMENT: A Formal Framework for MOdel ManageMENT. PhD thesis, Universitat Politècnica de València, Spain (2007)
[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)
[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) · Zbl 05535521 · doi:10.1007/978-3-642-00593-0_2
[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) · doi:10.1007/978-3-642-02571-6_7
[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)
[20] Boronat, A., Meseguer, J.: An algebraic semantics for MOF. Formal Aspects of Computing 22(3-4), 269–296 (2010) · Zbl 1213.68358 · doi:10.1007/s00165-009-0140-9
[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) · Zbl 05682212 · doi:10.1007/978-3-642-12029-9_3
[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)
[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)
[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) · Zbl 1278.68166 · doi:10.1007/3-540-45013-0_21
[25] Braga, C., Meseguer, J.: Modular rewriting semantics in practice. In: Proc. WRLA 2004. ENTCS, vol. 117, pp. 393–416. Elsevier, Amsterdam (2004) · Zbl 1272.68168
[26] Broy, M., Wirsing, M., Pepper, P.: On the algebraic definition of programming languages. ACM TOPLAS 9(1), 54–99 (1987) · Zbl 0627.68009 · doi:10.1145/9758.10501
[27] Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1-3), 386–414 (2006) · Zbl 1097.68051 · doi:10.1016/j.tcs.2006.04.012
[28] Chalub, F.: An implementation of Modular SOS in Maude. Master’s thesis, Universidade Federal Fluminense, Niterói, RJ, Brazil (May 2005)
[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)
[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) · Zbl 1038.68548 · doi:10.1007/3-540-44881-0_15
[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) · Zbl 1115.68046
[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) · Zbl 05547665 · doi:10.1007/11784180_28
[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)
[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
[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)
[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) · Zbl 1253.68211 · doi:10.1007/978-3-642-03429-9_10
[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)
[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) · Zbl 1103.68611 · doi:10.1007/978-3-540-27813-9_46
[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) · Zbl 1279.68207 · doi:10.1016/j.entcs.2007.06.008
[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) · Zbl 1108.68382 · doi:10.1007/978-3-540-27815-3_14
[43] Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the {\(\lambda\)}-calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts, Denmark, pp. 193–219 (August 1986)
[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)
[45] Friedman, D.P., Wand, M., Haynes, C.T.: Essentials of Programming Languages, 2nd edn. MIT Press, Cambridge (2001) · Zbl 0994.68020
[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)
[47] Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996) · Zbl 0887.68066
[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)
[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) · Zbl 0467.68014 · doi:10.1007/3-540-10699-5_106
[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)
[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) · Zbl 0788.68018 · doi:10.1007/3-540-56992-8_17
[52] Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060
[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)
[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) · Zbl 1279.68116
[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) · Zbl 1272.68186
[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) · Zbl 0635.68007 · doi:10.1007/BFb0039592
[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) · Zbl 1306.68078 · doi:10.1007/978-3-642-16310-4_10
[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) · Zbl 1279.68189
[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) · Zbl 1325.68150
[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)
[61] Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, Dordrecht (2000)
[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) · doi:10.1016/B978-044450556-9/50065-4
[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)
[64] Lee, E.A.: Modeling concurrent real-time processes using discrete events. Ann. Software Eng. 7, 25–45 (1999) · Zbl 05466731 · doi:10.1023/A:1018998524196
[65] Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Proc. POPL 1995, pp. 333–343. ACM Press, New York (1995)
[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) · doi:10.1007/978-94-017-0464-9_1
[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)
[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)
[69] Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992) · Zbl 0758.68043 · doi:10.1016/0304-3975(92)90182-F
[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) · doi:10.1007/3-540-61604-7_64
[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) · Zbl 0903.08009 · doi:10.1007/3-540-64299-4_26
[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)
[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) · Zbl 1108.68401 · doi:10.1007/978-3-540-27815-3_29
[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)
[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) · Zbl 05854655 · doi:10.1007/978-3-642-16901-4_21
[76] Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoretical Computer Science 373, 213–237 (2007) · Zbl 1111.68068 · doi:10.1016/j.tcs.2006.12.018
[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) · doi:10.1007/978-3-540-25984-8_1
[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) · Zbl 1222.68113 · doi:10.1007/11814771_3
[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)
[80] Misra, J., Cook, W.R.: Computation orchestration. Software and System Modeling 6(1), 83–110 (2007) · Zbl 05149645 · doi:10.1007/s10270-006-0012-1
[81] Moggi, E.: An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Edinburgh University, Dept. of Computer Science (June 1989)
[82] Mokhati, F., Badri, M.: Generating Maude specifications from UML use case diagrams. Journal of Object Technology 8(2), 319–136 (2009) · Zbl 05738567 · doi:10.5381/jot.2009.8.2.a2
[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)
[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) · Zbl 05739112 · doi:10.5381/jot.2010.9.3.a2
[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) · doi:10.1007/BFb0028970
[86] Mosses, P.D.: Denotational semantics. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, ch. 11, North-Holland, Amsterdam (1990) · Zbl 0900.68295
[87] Mosses, P.D.: Modular structural operational semantics. J. Log. Algebr. Program. 60-61, 195–228 (2004) · Zbl 1072.68061 · doi:10.1016/j.jlap.2004.03.008
[88] Nadathur, G., Miller, D.: An overview of {\(\lambda\)}Prolog. In: Bowen, K., Kowalski, R. (eds.) Fifth Int. Joint Conf. and Symp. on Logic Programming, pp. 810–827. The MIT Press, Cambridge (1988)
[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) · doi:10.1007/3-540-48118-4_38
[90] Nakajima, S., Futatsugi, K.: An object-oriented modeling method for algebraic specifications in CafeOBJ. In: Proc. ICSE 1997. ACM, New York (1997)
[91] Norrish, M.: C formalised in HOL. Technical Report UCAM-CL-TR-453, University of Cambridge (December 1998)
[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) · Zbl 05724090 · doi:10.1007/978-3-642-13464-7_5
[93] Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theoretical Computer Science 285(2), 359–405 (2002) · Zbl 1001.68061 · doi:10.1016/S0304-3975(01)00363-2
[94] Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007) · Zbl 1115.68095 · doi:10.1007/s10990-007-9001-5
[95] Papaspyrou, N.S.: A Formal Semantics for the C Programming Language. PhD thesis, National Technical University of Athens (February 1998)
[96] Papaspyrou, N.S.: Denotational semantics of ANSI C. Computer Standards and Interfaces 23(3), 169–185 (2001) · doi:10.1016/S0920-5489(01)00059-9
[97] Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proc. PLDI 1988, pp. 199–208. ACM Press, New York (1988)
[98] Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002) · Zbl 0995.68018
[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) · Zbl 1072.68063 · doi:10.1016/j.jlap.2004.03.009
[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) · Zbl 1306.68086 · doi:10.1007/978-3-642-16310-4_12
[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)
[102] Roşu, G., Ştefănescu, A.: Matching logic: A new program verification approach (nier track). In: Proc. ICSE 2011(2011) · doi:10.1145/1985793.1985928
[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) · Zbl 1308.68045 · doi:10.1007/978-3-642-17796-5_9
[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) · doi:10.1007/978-3-540-45069-6_30
[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) · Zbl 1214.68188 · doi:10.1016/j.jlap.2010.03.012
[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)
[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)
[108] Schmidt, D.A.: Denotational Semantics – A Methodology for Language Development. Allyn and Bacon, Boston (1986)
[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
[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) · Zbl 0268.68004
[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)
[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) · Zbl 1165.68041 · doi:10.1016/j.ic.2008.03.026
[113] Slonneger, K., Kurtz, B.L.: Formal Syntax and Semantics of Programming Languages. Addison-Wesley, Reading (1995) · Zbl 0844.68016
[114] Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001) · Zbl 0978.68033 · doi:10.1007/978-3-642-59495-3
[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) · Zbl 1272.68044
[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)
[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) · Zbl 1272.68322
[118] van Deursen, A., Heering, J., Klint, P.: Language Prototyping: An Algebraic Specification Approach. World Scientific, Singapore (1996) · Zbl 0962.68114 · doi:10.1142/3163
[119] Verdejo, A.: Maude como marco semántico ejecutable. PhD thesis, Facultad de Informática, Universidad Complutense, Madrid, Spain (2003)
[120] Verdejo, A., Martí-Oliet, N.: Implementing CCS in Maude 2. In: Proc. WRLA 2002. ENTCS, Elsevier, Amsterdam (2002)
[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) · Zbl 1086.68552 · doi:10.1007/s10703-005-2254-x
[122] Verdejo, A., Martí-Oliet, N.: Executable structural operational semantics in Maude. Journal of Logic and Algebraic Programming 67(1-2), 226–293 (2006) · Zbl 1088.68095 · doi:10.1016/j.jlap.2005.09.008
[123] Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285, 487–517 (2002) · Zbl 1001.68058 · doi:10.1016/S0304-3975(01)00366-8
[124] Wadler, P.: The essence of functional programming. In: Proc. POPL 1992, pp. 1–14. ACM Press, New York (1992)
[125] Wand, M.: First-order identities as a defining language. Acta Informatica 14, 337–357 (1980) · Zbl 0424.68022 · doi:10.1007/BF00286491
[126] Wehrman, I., Kitchin, D., Cook, W.R., Misra, J.: A timed semantics of Orc. Theor. Comput. Sci. 402(2-3), 234–248 (2008) · Zbl 1147.68436 · doi:10.1016/j.tcs.2008.04.037
[127] Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. In: Proc. WRLA 1996. ENTCS, vol. 4, pp. 322–360 (1996) · Zbl 1001.68024 · doi:10.1016/S1571-0661(04)00046-5
[128] Wirsing, M., Knapp, A.: A formal approach to object-oriented software engineering. Theoretical Computer Science 285(2), 519–560 (2002) · Zbl 1001.68024 · doi:10.1016/S0304-3975(01)00367-X
[129] Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation 115(1), 38–94 (1994) · Zbl 0938.68559 · doi:10.1006/inco.1994.1093
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.