×

Twenty years of rewriting logic. (English) Zbl 1267.03043

This very dense paper touches upon many, if not all, aspects of rewriting logic: 476 references are cited in the 49 pages of the paper. The first sections of the paper could be read as a dense introduction to rewriting logic, but, first and foremost, the paper is a survey paper in style and scope. Thus, the most likely reader is a researcher in rewriting logic who wishes to broaden his view of the field or find related work.

MSC:

03B70 Logic in computer science
68Q42 Grammars and rewriting systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aziz, A.; Singhal, V.; Brayton, R. K.; Sangiovanni-Vincentelli, A. L., It usually works: the temporal logic of stochastic systems, (Wolper, P., 7th International Conference On Computer Aided Verification, vol. 939 (1995), Springer Verlag: Springer Verlag Liege, Belgium), 155-165
[2] Abate, A.; Bai, Y.; Sznajder, N.; Talcott, C. L.; Tiwari, A., Quantitative and probabilistic modeling in pathway logic, (Zhu, M. M.; Zhang, Y.; Arabnia, H. R.; Deng, Y., Proceedings of the 7th IEEE International Conference on Bioinformatics and Bioengineering, BIBE 2007, Harvard Medical School, Boston, MA, USA, October 14-17, 2007 (2007), IEEE), 922-929
[3] Agha, G., Actors (1986), MIT Press
[4] G.A. Agha, M. Greenwald, C.A. Gunter, S. Khanna, J. Meseguer, K. Sen, P. Thati, Formal modeling and analysis of DoS using probabilistic rewrite theories, in: A. Sabelfeld (Ed.), Proceedings of the Workshop on Foundations of Computer Security, FCS’05, (Affiliated with LICS’05), Chicago, IL, June 30-July 1, 2005, 2005, pp. 91-102.; G.A. Agha, M. Greenwald, C.A. Gunter, S. Khanna, J. Meseguer, K. Sen, P. Thati, Formal modeling and analysis of DoS using probabilistic rewrite theories, in: A. Sabelfeld (Ed.), Proceedings of the Workshop on Foundations of Computer Security, FCS’05, (Affiliated with LICS’05), Chicago, IL, June 30-July 1, 2005, 2005, pp. 91-102.
[5] Agha, G. A.; Meseguer, J.; Sen, K., PMaude: rewrite-based specification language for probabilistic object systems, (Cerone, A.; Wiklicky, H., Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 2005, Edinburgh, UK, April 2-3, 2005. Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 2005, Edinburgh, UK, April 2-3, 2005, Electronic Notes in Theoretical Computer Science, vol. 153(2) (2006), Elsevier), 213-239
[6] O. Agrigoroaiei, G. Ciobanu, Rewriting logic specification of membrane systems with promoters and inhibitors, in Roşu [403], pp. 5-22.; O. Agrigoroaiei, G. Ciobanu, Rewriting logic specification of membrane systems with promoters and inhibitors, in Roşu [403], pp. 5-22. · Zbl 1347.68125
[7] Ahrendt, W.; Roth, A.; Sasse, R., Automatic validation of transformation rules for Java verification against a rewriting semantics, (Sutcliffe, G.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings. Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3835 (2005), Springer), 412-426 · Zbl 1143.68348
[8] Alarcón, B.; Gutiérrez, R.; Lucas, S., Context-sensitive dependency pairs, Information and Computation, 208, 8, 922-968 (2010) · Zbl 1206.68158
[9] B. Alarcón, R. Gutiérrez, S. Lucas, R. Navarro-Marset, Proving termination properties with MU-TERM, in Johnson and Pavlovic [246], pp. 201-208.; B. Alarcón, R. Gutiérrez, S. Lucas, R. Navarro-Marset, Proving termination properties with MU-TERM, in Johnson and Pavlovic [246], pp. 201-208.
[10] B. Alarcón, S. Lucas, J. Meseguer, A dependency pair framework for A \(\operatorname{\vee;} \); B. Alarcón, S. Lucas, J. Meseguer, A dependency pair framework for A \(\operatorname{\vee;} \)
[11] Alba-Castro, M.; Alpuente, M.; Escobar, S., Abstract certification of global non-interference in rewriting logic, (Leuschel, M.; Hallerstede, S.; de Boer, F.; Bonsangue, M., Formal Methods for Components and Objects, 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009, Revised Selected Papers. Formal Methods for Components and Objects, 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6286 (2010), Springer), 105-124 · Zbl 1312.68049
[12] Alba-Castro, M.; Alpuente, M.; Escobar, S., Approximating non-interference and erasure in rewriting logic, (Ida, T., Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010, Timisoara, Romania, September 23-26, 2010 (2010), IEEE Computer Society), 124-132
[13] A. Albarrán, F. Durán, A. Vallecillo, From Maude specifications to SOAP distributed implementations: a smooth transition, in: O. Dı´az, A. Illarramendi, M. Piattini (Eds.), Actas de las VI Jornadas de Ingenierı´a del Software y Bases de Datos, JISBD 2001, Almagro (Ciudad Real), España, Noviembre 21-23, 2001, 2001, pp. 419-434.; A. Albarrán, F. Durán, A. Vallecillo, From Maude specifications to SOAP distributed implementations: a smooth transition, in: O. Dı´az, A. Illarramendi, M. Piattini (Eds.), Actas de las VI Jornadas de Ingenierı´a del Software y Bases de Datos, JISBD 2001, Almagro (Ciudad Real), España, Noviembre 21-23, 2001, 2001, pp. 419-434.
[14] A. Albarrán, F. Durán, A. Vallecillo, Maude meets CORBA, in: G. Fernandez, C. Pons (Eds.), Proceedings of the Second Argentine Symposium on Software Engineering, ASSE 2001, Buenos Aires, Argentina, September 10-11, 2001, 2001.; A. Albarrán, F. Durán, A. Vallecillo, Maude meets CORBA, in: G. Fernandez, C. Pons (Eds.), Proceedings of the Second Argentine Symposium on Software Engineering, ASSE 2001, Buenos Aires, Argentina, September 10-11, 2001, 2001.
[15] Alpuente, M.; Ballis, D.; Romero, D., Specification and verification of web applications in rewriting logic, (Cavalcanti, A.; Dams, D., FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings. FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5850 (2009), Springer), 790-805
[16] Alpuente, M.; Escobar, S.; Meseguer, J.; Ojeda, P., A modular equational generalization algorithm, (Hanus, M., Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers. Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers, Lecture Notes in Computer Science, vol. 5438 (2009), Springer), 24-39 · Zbl 1185.68219
[17] Alpuente, M.; Escobar, S.; Meseguer, J.; Ojeda, P., Order-sorted generalization, (Falaschi, M., Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2008, Siena, Italy, July 3-4, 2008. Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming, WFLP 2008, Siena, Italy, July 3-4, 2008, Electronic Notes in Theoretical Computer Science, vol. 246 (2009), Elsevier), 27-38 · Zbl 1347.68193
[18] M. AlTurki, Rewriting-based formal modeling, analysis and implementation of real-time distributed services, Ph.D. thesis, University of Illinois at Urbana-Champaign, 2011. Available from: <http://hdl.handle.net/2142/26231>; M. AlTurki, Rewriting-based formal modeling, analysis and implementation of real-time distributed services, Ph.D. thesis, University of Illinois at Urbana-Champaign, 2011. Available from: <http://hdl.handle.net/2142/26231>
[19] M. AlTurki, D. Dhurjati, D. Yu, A. Chander, H. Inamura, Formal specification and analysis of timing properties in software systems, in Chechik and Wirsing [90], pp. 262-277.; M. AlTurki, D. Dhurjati, D. Yu, A. Chander, H. Inamura, Formal specification and analysis of timing properties in software systems, in Chechik and Wirsing [90], pp. 262-277.
[20] M. AlTurki, J. Meseguer, Real-time rewriting semantics of Orc, in Leuschel and Podelski [284], pp. 131-142.; M. AlTurki, J. Meseguer, Real-time rewriting semantics of Orc, in Leuschel and Podelski [284], pp. 131-142. · Zbl 1329.68169
[21] AlTurki, M.; Meseguer, J., Reduction semantics and formal analysis of Orc programs, (Ballis, D.; Escobar, S.; Marchiori, M., Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, WWV 2007, Venice, Italy, December 14, 2007. Proceedings of the 3rd International Workshop on Automated Specification and Verification of Web Systems, WWV 2007, Venice, Italy, December 14, 2007, Electronic Notes in Theoretical Computer Science, vol. 200(3) (2008), Elsevier), 25-41
[22] M. AlTurki, J. Meseguer, Dist-Orc: a rewriting-based distributed implementation of Orc with formal analysis, in Ölveczky [361], pp. 26-45.; M. AlTurki, J. Meseguer, Dist-Orc: a rewriting-based distributed implementation of Orc with formal analysis, in Ölveczky [361], pp. 26-45.
[23] M. AlTurki, J. Meseguer, PVeStA: a parallel statistical model checking and quantitative analysis tool, in Corradini et al. [124], pp. 386-392.; M. AlTurki, J. Meseguer, PVeStA: a parallel statistical model checking and quantitative analysis tool, in Corradini et al. [124], pp. 386-392.
[24] M. AlTurki, J. Meseguer, C.A. Gunter, Probabilistic modeling and analysis of DoS protection for the ASV protocol, in Dougherty and Escobar [144], pp. 3-18.; M. AlTurki, J. Meseguer, C.A. Gunter, Probabilistic modeling and analysis of DoS protection for the ASV protocol, in Dougherty and Escobar [144], pp. 3-18.
[25] Alur, R.; Courcoubetis, C.; Dill, D. L., Model-checking for real-time systems, (LICS’90 (1990), IEEE), 414-425
[26] Alur, R.; Dill, D. L., A theory of timed automata, Theoretical Computer Science, 126, 2, 83-235 (1994) · Zbl 0803.68071
[27] Anastasio, T. J., Data-driven modeling of Alzheimer disease pathogenesis, Journal of Theoretical Biology, 290, 60-72 (2011) · Zbl 1397.92310
[28] Andrei, O.; Ciobanu, G.; Lucanu, D., A rewriting logic framework for operational semantics of membrane systems, Theoretical Computer Science, 373, 3, 163-181 (2007) · Zbl 1111.68064
[29] Andrei, O.; Ib&abreve;nescu, L.; Kirchner, H., Non-intrusive formal methods and strategic rewriting for a chemical application, (Futatsugi, K.; Jouannaud, J.-P.; Meseguer, J., Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday. Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 4060 (2006), Springer), 194-215 · Zbl 1132.68319
[30] Andrei, O.; Kirchner, H., Graph rewriting and strategies for modeling biochemical networks, (Negru, V.; Jebelean, T.; Petcu, D.; Zaharie, D., Proceedings of the Ninth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2007, Timisoara, Romania, September 26-29, 2007 (2007), IEEE Computer Society), 407-414
[31] Andrei, O.; Kirchner, H., A port graph calculus for autonomic computing and invariant verification, Electronic Notes in Theoretical Computer Science, 253, 4, 17-38 (2009) · Zbl 1291.68241
[32] O. Andrei, D. Lucanu, Strategy-based proof calculus for membrane systems, in Roşu [403], pp. 23-43.; O. Andrei, D. Lucanu, Strategy-based proof calculus for membrane systems, in Roşu [403], pp. 23-43. · Zbl 1347.68126
[33] Aoumeur, N.; Saake, G., Integrating and rapid-prototyping UML structural and behavioural diagrams using rewriting logic, (Pidduck, A. B.; Mylopoulos, J.; Woo, C. C.; Özsu, M. T., Advanced Information Systems Engineering, 14th International Conference, CAiSE 2002, Toronto, Canada, May 27-31, 2002, Proceedings. Advanced Information Systems Engineering, 14th International Conference, CAiSE 2002, Toronto, Canada, May 27-31, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2348 (2002), Springer), 296-310 · Zbl 1046.68663
[34] Avron, A.; Honsell, F.; Mason, I. A.; Pollack, R., Using typed lambda calculus to implement formal systems on a machine, Journal of Automated Reasoning, 9, 3, 309-354 (1992) · Zbl 0784.68072
[35] (Baader, F., Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings. Term Rewriting and Applications, 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4533 (2007), Springer) · Zbl 1121.68001
[36] (Backes, M.; Ning, P., Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009, Proceedings. Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5789 (2009), Springer) · Zbl 1477.68009
[37] K. Bae, J. Meseguer, A rewriting-based model checker for the temporal logic of rewriting, in Kniesel and Pinto [270], pp. 46-60.; K. Bae, J. Meseguer, A rewriting-based model checker for the temporal logic of rewriting, in Kniesel and Pinto [270], pp. 46-60. · Zbl 1291.68244
[38] K. Bae, J. Meseguer, The linear temporal logic of rewriting Maude model checker, in Ölveczky [362], pp. 208-225.; K. Bae, J. Meseguer, The linear temporal logic of rewriting Maude model checker, in Ölveczky [362], pp. 208-225. · Zbl 1306.68099
[39] K. Bae, J. Meseguer, State/event-based LTL model checking under parametric generalized fairness, in: G. Gopalakrishnan, S. Qadeer (Eds.), Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings, Lecture Notes in Computer Science, vol. 6806, Springer, 2011, pp. 132-148.; K. Bae, J. Meseguer, State/event-based LTL model checking under parametric generalized fairness, in: G. Gopalakrishnan, S. Qadeer (Eds.), Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011, Proceedings, Lecture Notes in Computer Science, vol. 6806, Springer, 2011, pp. 132-148.
[40] K. Bae, P.C. Ölveczky, Extending the Real-Time Maude semantics of Ptolemy to hierarchical DE models, in Ölveczky [361], pp. 46-66.; K. Bae, P.C. Ölveczky, Extending the Real-Time Maude semantics of Ptolemy to hierarchical DE models, in Ölveczky [361], pp. 46-66.
[41] K. Bae, P.C. Ölveczky, A. Al-Nayeem, J. Meseguer, Synchronous AADL and its formal analysis in Real-Time Maude, Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, 2011.; K. Bae, P.C. Ölveczky, A. Al-Nayeem, J. Meseguer, Synchronous AADL and its formal analysis in Real-Time Maude, Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, 2011.
[42] K. Bae, P.C. Ölveczky, T.H. Feng, S. Tripakis, Verifying Ptolemy II discrete-event models using Real-Time Maude, in: K. Breitman, A. Cavalcanti (Eds.), Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5885, Springer, 2009, pp. 717-736.; K. Bae, P.C. Ölveczky, T.H. Feng, S. Tripakis, Verifying Ptolemy II discrete-event models using Real-Time Maude, in: K. Breitman, A. Cavalcanti (Eds.), Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5885, Springer, 2009, pp. 717-736. · Zbl 1264.68051
[43] C. Baier, J.-P. Katoen, H. Hermanns, Approximate symbolic model checking of continuous-time markov chains, in: CONCUR’99, LNCS, vol. 1664, Springer, 1999, pp. 146-161.; C. Baier, J.-P. Katoen, H. Hermanns, Approximate symbolic model checking of continuous-time markov chains, in: CONCUR’99, LNCS, vol. 1664, Springer, 1999, pp. 146-161. · Zbl 0934.03044
[44] H. Baker, C. Hewitt, Laws for communicating parallel processes, in: Proceedings of the 1977 IFIP Congress, IFIP Press, 1977, pp. 987-992.; H. Baker, C. Hewitt, Laws for communicating parallel processes, in: Proceedings of the 1977 IFIP Congress, IFIP Press, 1977, pp. 987-992. · Zbl 0363.68077
[45] Baldan, P.; Bertolissi, C.; Cirstea, H.; Kirchner, C., A rewriting calculus for cyclic higher-order term graphs, Mathematical Structures in Computer Science, 17, 3, 363-406 (2007) · Zbl 1125.68062
[46] E. Balland, P. Brauner, R. Kopetz, P.-E. Moreau, A. Reilles, Tom: Piggybacking rewriting on Java, in Baader [35], pp. 36-47.; E. Balland, P. Brauner, R. Kopetz, P.-E. Moreau, A. Reilles, Tom: Piggybacking rewriting on Java, in Baader [35], pp. 36-47.
[47] Banâtre, J.-P.; Mètayer, D. L., The Gamma model and its discipline of programming, Science of Computer Programming, 15, 55-77 (1990) · Zbl 0715.68054
[48] Barker, S.; Fernández, M., Term rewriting for access control, (Damiani, E.; Liu, P., DBSec. DBSec, Lecture Notes in Computer Science, vol. 4127 (2006), Springer), 179-193
[49] G. Barthe, F.S. de Boer (Eds.), Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5051, Springer, 2008.; G. Barthe, F.S. de Boer (Eds.), Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5051, Springer, 2008.
[50] Basin, D.; Clavel, M.; Meseguer, J., Reflective metalogical frameworks, ACM Transactions on Computational Logic, 5, 3, 528-576 (2004) · Zbl 1407.03045
[51] Basin, D. A.; Constable, R. L., Metalogical frameworks, (Huet, G.; Plotkin, G., Logical Environments (1993), Cambridge University Press), 1-29 · Zbl 0922.03019
[52] E. Beffara, O. Bournez, H. Kacem, C. Kirchner, Verification of timed automata using rewrite rules and strategies, in: N. Dershowitz, A. Frank (Eds.), Proceedings of the Seventh Biennial Bar-Ilan International Symposium on the Foundations of Artificial Intelligence, BISFAI 2001, Ramat-Gan, Israel, June 25-27, 2001, Computing Research Repository (CoRR), 2001.; E. Beffara, O. Bournez, H. Kacem, C. Kirchner, Verification of timed automata using rewrite rules and strategies, in: N. Dershowitz, A. Frank (Eds.), Proceedings of the Seventh Biennial Bar-Ilan International Symposium on the Foundations of Artificial Intelligence, BISFAI 2001, Ramat-Gan, Israel, June 25-27, 2001, Computing Research Repository (CoRR), 2001.
[53] S. Berardi, Towards a mathematical analysis of the Coquand-Huet calculus of constructions and other systems in Barendregt’s cube, Technical report, Carnegie-Mellon University and Università di Torino, 1988.; S. Berardi, Towards a mathematical analysis of the Coquand-Huet calculus of constructions and other systems in Barendregt’s cube, Technical report, Carnegie-Mellon University and Università di Torino, 1988.
[54] J. Bergstra, J. Tucker, Characterization of computable data types by means of a finite equational specification method, in: J.W. de Bakker, J. van Leeuwen (Eds.), Automata, Languages and Programming, Seventh Colloquium, LNCS, vol. 81, Springer-Verlag, 1980, pp. 76-90.; J. Bergstra, J. Tucker, Characterization of computable data types by means of a finite equational specification method, in: J.W. de Bakker, J. van Leeuwen (Eds.), Automata, Languages and Programming, Seventh Colloquium, LNCS, vol. 81, Springer-Verlag, 1980, pp. 76-90. · Zbl 0449.68003
[55] Berry, G.; Boudol, G., The chemical abstract machine, Theoretical Computer Science, 96, 1, 217-248 (1992) · Zbl 0747.68013
[56] C. Bertolissi, H. Cirstea, C. Kirchner, Translating combinatory reduction systems into the rewriting calculus, in: J.-L. Giavitto, P.-E. Moreau (Eds.), Proceedings of the 4th International Workshop on Rule-Based Programming, RULE 2003, Valencia, Spain, June 9, 2003, Electronic Notes in Theoretical Computer Science, vol. 86(2), Elsevier, 2003, pp. 28-44.; C. Bertolissi, H. Cirstea, C. Kirchner, Translating combinatory reduction systems into the rewriting calculus, in: J.-L. Giavitto, P.-E. Moreau (Eds.), Proceedings of the 4th International Workshop on Rule-Based Programming, RULE 2003, Valencia, Spain, June 9, 2003, Electronic Notes in Theoretical Computer Science, vol. 86(2), Elsevier, 2003, pp. 28-44.
[57] Best, E.; Devillers, R., Sequential and concurrent behavior in Petri net theory, Theoretical Computer Science, 55, 87-136 (1989) · Zbl 0669.68043
[58] J. Bjørk, E.B. Johnsen, O. Owe, R. Schlatte, Lightweight time modeling in timed Creol, in Ölveczky [361], pp. 67-81.; J. Bjørk, E.B. Johnsen, O. Owe, R. Schlatte, Lightweight time modeling in timed Creol, in Ölveczky [361], pp. 67-81.
[59] M.M. Bonsangue, E.B. Johnsen (Eds.), Formal Methods for Open Object-Based Distributed Systems, 9th IFIP WG 6.1 International Conference, FMOODS 2007, Paphos, Cyprus, June 6-8, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4468, Springer, 2007.; M.M. Bonsangue, E.B. Johnsen (Eds.), Formal Methods for Open Object-Based Distributed Systems, 9th IFIP WG 6.1 International Conference, FMOODS 2007, Paphos, Cyprus, June 6-8, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4468, Springer, 2007.
[60] A. Boronat, MOMENT: A Formal Framework for MOdel ManageMENT, Ph.D. thesis, Universitat Politècnica de València, Spain, 2007.; A. Boronat, MOMENT: A Formal Framework for MOdel ManageMENT, Ph.D. thesis, Universitat Politècnica de València, Spain, 2007.
[61] A. Boronat, J.A. Carsı´, I. Ramos, Automatic reengineering in MDA using rewriting logic as transformation engine, in: N. Gold, T. Systä (Eds.), Proceedings of the 9th European Conference on Software Maintenance and Reengineering, CSMR 2005, Manchester, UK, March 21-23, 2005, Proceedings, IEEE Computer Society, 2005, pp. 228-231.; A. Boronat, J.A. Carsı´, I. Ramos, Automatic reengineering in MDA using rewriting logic as transformation engine, in: N. Gold, T. Systä (Eds.), Proceedings of the 9th European Conference on Software Maintenance and Reengineering, CSMR 2005, Manchester, UK, March 21-23, 2005, Proceedings, IEEE Computer Society, 2005, pp. 228-231.
[62] A. Boronat, R. Heckel, J. Meseguer, Rewriting logic semantics and verification of model transformations, in Chechik and Wirsing [90], pp. 18-33.; A. Boronat, R. Heckel, J. Meseguer, Rewriting logic semantics and verification of model transformations, in Chechik and Wirsing [90], pp. 18-33.
[63] A. Boronat, A. Knapp, J. Meseguer, M. Wirsing, What is a multi-modeling language? In Corradini and Montanari [125], pp. 71-87.; A. Boronat, A. Knapp, J. Meseguer, M. Wirsing, What is a multi-modeling language? In Corradini and Montanari [125], pp. 71-87. · Zbl 1253.68225
[64] A. Boronat, J. Meseguer, Algebraic semantics of OCL-constrained metamodel specifications, in: M. Oriol, B. Meyer (Eds.), Objects, Components, Models and Patterns, 47th International Conference, TOOLS EUROPE 2009, Zurich, Switzerland, June 29-July 3, 2009, Proceedings, Lecture Notes in Business Information Processing, vol. 33, Springer, 2009, pp. 96-115.; A. Boronat, J. Meseguer, Algebraic semantics of OCL-constrained metamodel specifications, in: M. Oriol, B. Meyer (Eds.), Objects, Components, Models and Patterns, 47th International Conference, TOOLS EUROPE 2009, Zurich, Switzerland, June 29-July 3, 2009, Proceedings, Lecture Notes in Business Information Processing, vol. 33, Springer, 2009, pp. 96-115.
[65] A. Boronat, J. Meseguer, MOMENT2: EMF model transformations in Maude, in A. Vallecillo, G. Sagardui (Eds.), Actas de las XIV Jornadas de Ingenierı´a del Software y Bases de Datos, JISBD 2009, San Sebastián, España, Septiembre 8-11, 2009, 2009, pp. 178-179.; A. Boronat, J. Meseguer, MOMENT2: EMF model transformations in Maude, in A. Vallecillo, G. Sagardui (Eds.), Actas de las XIV Jornadas de Ingenierı´a del Software y Bases de Datos, JISBD 2009, San Sebastián, España, Septiembre 8-11, 2009, 2009, pp. 178-179.
[66] Boronat, A.; Meseguer, J., An algebraic semantics for MOF, Formal Aspects of Computing, 22, 3-4, 269-296 (2010) · Zbl 1213.68358
[67] A. Boronat, P.C. Ölveczky, Formal real-time model transformations in MOMENT2, in: D.S. Rosenblum, G. Taentzer (Eds.), Fundamental Approaches to Software Engineering, 13th International Conference, FASE 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6013, Springer, 2010, pp. 29-43.; A. Boronat, P.C. Ölveczky, Formal real-time model transformations in MOMENT2, in: D.S. Rosenblum, G. Taentzer (Eds.), Fundamental Approaches to Software Engineering, 13th International Conference, FASE 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6013, Springer, 2010, pp. 29-43.
[68] P. Borovanský, C. Castro, Cooperation of constraint solvers: using the new process control facilities of ELAN, in Kirchner and Kirchner [262], pp. 1-20.; P. Borovanský, C. Castro, Cooperation of constraint solvers: using the new process control facilities of ELAN, in Kirchner and Kirchner [262], pp. 1-20.
[69] P. Borovanský, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, Q.-H. Nguyen, C. Ringeissen, M. Vittek, ELAN v 3.6 user manual, Technical report, INRIA Lorraine & LORIA, Nancy, France, February 2004.; P. Borovanský, H. Cirstea, H. Dubois, C. Kirchner, H. Kirchner, P.-E. Moreau, Q.-H. Nguyen, C. Ringeissen, M. Vittek, ELAN v 3.6 user manual, Technical report, INRIA Lorraine & LORIA, Nancy, France, February 2004.
[70] Borovanský, P.; Kirchner, C.; Kirchner, H.; Moreau, P.-E., ELAN from a rewriting logic point of view, Theoretical Computer Science, 285, 2, 155-185 (2002) · Zbl 1001.68057
[71] Borovanský, P.; Kirchner, C.; Kirchner, H.; Ringeissen, C., Rewriting with strategies in ELAN: a functional semantics, International Journal of Foundations of Computer Science, 12, 1, 69-95 (2001) · Zbl 1319.68125
[72] Bouhoula, A.; Jouannaud, J.-P.; Meseguer, J., Specification and proof in membership equational logic, Theoretical Computer Science, 236, 1-2, 35-132 (2000) · Zbl 0938.68057
[73] O. Bournez, G.-M. Côme, V. Conraud, H. Kirchner, L. Ibănescu, A rule-based approach for automated generation of kinetic chemical mechanisms, in Nieuwenhuis [355], pp. 30-45.; O. Bournez, G.-M. Côme, V. Conraud, H. Kirchner, L. Ibănescu, A rule-based approach for automated generation of kinetic chemical mechanisms, in Nieuwenhuis [355], pp. 30-45.
[74] O. Bournez, M. Hoyrup, Rewriting logic and probabilities, in Nieuwenhuis [355], pp. 61-75.; O. Bournez, M. Hoyrup, Rewriting logic and probabilities, in Nieuwenhuis [355], pp. 61-75. · Zbl 1038.68063
[75] O. Bournez, L. Ibănescu, H. Kirchner, From chemical rules to term rewriting, in: H. Cirstea, N. Martı´-Oliet (Eds.), Proceedings of the 6th International Workshop on Rule-Based Programming, RULE 2005, Nara, Japan, April 23, 2005, Electronic Notes in Theoretical Computer Science, vol. 147(1), Elsevier, 2006, pp. 113-134.; O. Bournez, L. Ibănescu, H. Kirchner, From chemical rules to term rewriting, in: H. Cirstea, N. Martı´-Oliet (Eds.), Proceedings of the 6th International Workshop on Rule-Based Programming, RULE 2005, Nara, Japan, April 23, 2005, Electronic Notes in Theoretical Computer Science, vol. 147(1), Elsevier, 2006, pp. 113-134.
[76] O. Bournez, C. Kirchner, Probabilistic rewrite strategies. Applications to ELAN, in: S. Tison (Ed.), Rewriting Techniques and Applications, 13th International Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2378, Springer, 2002, pp. 252-266.; O. Bournez, C. Kirchner, Probabilistic rewrite strategies. Applications to ELAN, in: S. Tison (Ed.), Rewriting Techniques and Applications, 13th International Conference, RTA 2002, Copenhagen, Denmark, July 22-24, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2378, Springer, 2002, pp. 252-266. · Zbl 1045.68577
[77] C. Braga, J. Meseguer, Modular rewriting semantics in practice, in: Martı´-Oliet [297], pp. 393-416.; C. Braga, J. Meseguer, Modular rewriting semantics in practice, in: Martı´-Oliet [297], pp. 393-416. · Zbl 1272.68168
[78] R. Bruni, Tile Logic for Synchronized Rewriting of Concurrent Systems, Ph.D. thesis, Dipartimento di Informatica, Università di Pisa, 1999, Technical report TD-1/99.; R. Bruni, Tile Logic for Synchronized Rewriting of Concurrent Systems, Ph.D. thesis, Dipartimento di Informatica, Università di Pisa, 1999, Technical report TD-1/99.
[79] R. Bruni, J. Meseguer, Generalized rewrite theories, in: J.C.M. Baeten, J.K. Lenstra, J. Parrow, G.J. Woeginger (Eds.), Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30-July 4, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2719, Springer, 2003, pp. 252-266.; R. Bruni, J. Meseguer, Generalized rewrite theories, in: J.C.M. Baeten, J.K. Lenstra, J. Parrow, G.J. Woeginger (Eds.), Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30-July 4, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2719, Springer, 2003, pp. 252-266. · Zbl 1039.03020
[80] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theoretical Computer Science, 360, 1-3, 386-414 (2006) · Zbl 1097.68051
[81] Bruni, R.; Meseguer, J.; Montanari, U., Symmetric monoidal and cartesian double categories as a semantic framework for tile logic, Mathematical Structures in Computer Science, 12, 1, 53-90 (2002) · Zbl 0993.68058
[82] R. Bruni, J. Meseguer, U. Montanari, Tiling transactions in rewriting logic, in Gadducci and Montanari [205], pp. 90-109.; R. Bruni, J. Meseguer, U. Montanari, Tiling transactions in rewriting logic, in Gadducci and Montanari [205], pp. 90-109. · Zbl 1272.68291
[83] R. Bruni, U. Montanari, J. Meseguer, Internal strategies in a rewriting implementation of tile systems, in Kirchner and Kirchner [262], pp. 263-284.; R. Bruni, U. Montanari, J. Meseguer, Internal strategies in a rewriting implementation of tile systems, in Kirchner and Kirchner [262], pp. 263-284. · Zbl 0917.68104
[84] G. Carabetta, P. Degano, F. Gadducci, CCS semantics via proved transition systems and rewriting logic, in Kirchner and Kirchner [262], pp. 369-387.; G. Carabetta, P. Degano, F. Gadducci, CCS semantics via proved transition systems and rewriting logic, in Kirchner and Kirchner [262], pp. 369-387. · Zbl 0917.68126
[85] M. Casadei, L. Gardelli, M. Viroli, Simulating emergent properties of coordination in Maude: the collective sort case, in: C. Canal, M. Viroli (Eds.), Proceedings of the Fifth International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2006, Bonn, Germany, August 31, 2006, Electronic Notes in Theoretical Computer Science, vol. 175(2), Elsevier, 2007, pp. 59-80.; M. Casadei, L. Gardelli, M. Viroli, Simulating emergent properties of coordination in Maude: the collective sort case, in: C. Canal, M. Viroli (Eds.), Proceedings of the Fifth International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2006, Bonn, Germany, August 31, 2006, Electronic Notes in Theoretical Computer Science, vol. 175(2), Elsevier, 2007, pp. 59-80.
[86] M. Casadei, A. Omicini, M. Viroli, Prototyping A&A ReSpecT in Maude, in: C. Canal, P. Poizat, M. Viroli (Eds.), Proceedings of the 6th International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2007, Lisbon, Portugal, September 8, 2007, Electronic Notes in Theoretical Computer Science, vol. 194, Elsevier, 2008, pp. 93-109.; M. Casadei, A. Omicini, M. Viroli, Prototyping A&A ReSpecT in Maude, in: C. Canal, P. Poizat, M. Viroli (Eds.), Proceedings of the 6th International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2007, Lisbon, Portugal, September 8, 2007, Electronic Notes in Theoretical Computer Science, vol. 194, Elsevier, 2008, pp. 93-109.
[87] Cervesato, I.; Stehr, M.-O., Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types, Higher-Order and Symbolic Computation, 20, 1-2, 3-35 (2007) · Zbl 1115.68073
[88] R. Chadha, C.A. Gunter, J. Meseguer, R. Shankesi, M. Viswanathan, Modular preservation of safety properties by cookie-based DoS-protection wrappers, in Barthe and de Boer [49], pp. 39-58.; R. Chadha, C.A. Gunter, J. Meseguer, R. Shankesi, M. Viswanathan, Modular preservation of safety properties by cookie-based DoS-protection wrappers, in Barthe and de Boer [49], pp. 39-58.
[89] F. Chalub, C. Braga, Maude MSOS tool, in Denker and Talcott [139], pp. 133-146.; F. Chalub, C. Braga, Maude MSOS tool, in Denker and Talcott [139], pp. 133-146.
[90] M. Chechik, M. Wirsing (Eds.), Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5503, Springer, 2009.; M. Chechik, M. Wirsing (Eds.), Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5503, Springer, 2009. · Zbl 1157.68300
[91] F. Chen, G. Roşu, R.P. Venkatesan, Rule-based analysis of dimensional safety, in Nieuwenhuis [355], pp. 197-207.; F. Chen, G. Roşu, R.P. Venkatesan, Rule-based analysis of dimensional safety, in Nieuwenhuis [355], pp. 197-207.
[92] S. Chen, J. Meseguer, R. Sasse, H.J. Wang, Y.-M. Wang, A systematic approach to uncover security flaws in GUI logic, in: B. Pfitzmann, P. McDaniel (Eds.), Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), Oakland, California, USA, May 20-23, 2007, IEEE Computer Society, 2007, pp. 71-85.; S. Chen, J. Meseguer, R. Sasse, H.J. Wang, Y.-M. Wang, A systematic approach to uncover security flaws in GUI logic, in: B. Pfitzmann, P. McDaniel (Eds.), Proceedings of the 2007 IEEE Symposium on Security and Privacy (S&P 2007), Oakland, California, USA, May 20-23, 2007, IEEE Computer Society, 2007, pp. 71-85.
[93] S. Chen, K. Pattabiraman, Z. Kalbarczyk, R.K. Iyer, Formal reasoning of various categories of widely exploited security vulnerabilities by pointer taintedness semantics, in: Y. Deswarte, F. Cuppens, S. Jajodia, L. Wang (Eds.), 19th International Information Security Conference, SEC 2004, Toulouse, France, August 22-27, 2004, Proceedings, Kluwer, 2004, pp. 83-100.; S. Chen, K. Pattabiraman, Z. Kalbarczyk, R.K. Iyer, Formal reasoning of various categories of widely exploited security vulnerabilities by pointer taintedness semantics, in: Y. Deswarte, F. Cuppens, S. Jajodia, L. Wang (Eds.), 19th International Information Security Conference, SEC 2004, Toulouse, France, August 22-27, 2004, Proceedings, Kluwer, 2004, pp. 83-100.
[94] H. Cirstea, C. Kirchner, Theorem proving using computational systems: the case of the B predicate prover, Presented at CCL’97 Workshop, Schloss Dagstuhl, Germany, September 1997.; H. Cirstea, C. Kirchner, Theorem proving using computational systems: the case of the B predicate prover, Presented at CCL’97 Workshop, Schloss Dagstuhl, Germany, September 1997.
[95] Cirstea, H.; Kirchner, C., Combining higher-order and first-order computations using \(\rho \)-calculus: Towards a semantics of ELAN, (Gabbay, D.; de Rijke, M., Frontiers of Combining Systems. Frontiers of Combining Systems, Research Studies, vol. 2 (1999), Wiley), 95-120 · Zbl 1004.68080
[96] Cirstea, H.; Kirchner, C., The rewriting calculus - Part I, Logic Journal of the IGPL, 9, 3, 363-399 (2001)
[97] Cirstea, H.; Kirchner, C., The rewriting calculus - Part II, Logic Journal of the IGPL, 9, 3, 401-434 (2001)
[98] H. Cirstea, C. Kirchner, L. Liquori, The rho cube, in: F. Honsell, M. Miculan (Eds.), Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, 2001, Proceedings, Lecture Notes in Computer Science, vol. 2030, Springer, 2001, pp. 168-183.; H. Cirstea, C. Kirchner, L. Liquori, The rho cube, in: F. Honsell, M. Miculan (Eds.), Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, 2001, Proceedings, Lecture Notes in Computer Science, vol. 2030, Springer, 2001, pp. 168-183. · Zbl 0978.68072
[99] H. Cirstea, C. Kirchner, L. Liquori, Rewriting calculus with(out) types, in Gadducci and Montanari [205], pp. 3-19.; H. Cirstea, C. Kirchner, L. Liquori, Rewriting calculus with(out) types, in Gadducci and Montanari [205], pp. 3-19. · Zbl 1272.68173
[100] H. Cirstea, C. Kirchner, L. Liquori, B. Wack, Rewrite strategies in the rewriting calculus, in: B. Gramlich, S. Lucas (Eds.), Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2003, Valencia, Spain, June 8, 2003, Electronic Notes in Theoretical Computer Science, vol. 86(4), Elsevier, 2003, pp. 593-624.; H. Cirstea, C. Kirchner, L. Liquori, B. Wack, Rewrite strategies in the rewriting calculus, in: B. Gramlich, S. Lucas (Eds.), Proceedings of the 3rd International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2003, Valencia, Spain, June 8, 2003, Electronic Notes in Theoretical Computer Science, vol. 86(4), Elsevier, 2003, pp. 593-624. · Zbl 1270.68122
[101] Clarke, E. M.; Grumberg, O.; Peled, D. A., Model Checking (2001), MIT Press
[102] Clavel, M., Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications (2000), CSLI Publications · Zbl 1003.03032
[103] M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martı´-Oliet, J. Meseguer, C.L. Talcott, Unification and narrowing in Maude 2.4, in: R. Treinen (Ed.), Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brası´lia, Brazil, June 29-July 1, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5595, Springer, 2009, pp. 380-390.; M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln, N. Martı´-Oliet, J. Meseguer, C.L. Talcott, Unification and narrowing in Maude 2.4, in: R. Treinen (Ed.), Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brası´lia, Brazil, June 29-July 1, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5595, Springer, 2009, pp. 380-390.
[104] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı´-Oliet, J. Meseguer, Metalevel computation in Maude, in Kirchner and Kirchner [262], pp. 331-352.; M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martı´-Oliet, J. Meseguer, Metalevel computation in Maude, in Kirchner and Kirchner [262], pp. 331-352.
[105] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martı´-Oliet, N.; Meseguer, J.; Quesada, J. F., Maude: specification and programming in rewriting logic, Theoretical Computer Science, 285, 2, 187-243 (2002) · Zbl 1001.68059
[106] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martı´-Oliet, N.; Meseguer, J.; Talcott, C. L., (All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350 (2007), Springer) · Zbl 1115.68046
[107] M. Clavel, F. Durán, S. Eker, J. Meseguer, Building equational proving tools by reflection in rewriting logic, in Futatsugi et al. [203], pp. 1-31.; M. Clavel, F. Durán, S. Eker, J. Meseguer, Building equational proving tools by reflection in rewriting logic, in Futatsugi et al. [203], pp. 1-31.
[108] M. Clavel, F. Durán, S. Eker, J. Meseguer, M.-O. Stehr, Maude as a formal meta-tool, in Wing et al. [471], pp. 1684-1703.; M. Clavel, F. Durán, S. Eker, J. Meseguer, M.-O. Stehr, Maude as a formal meta-tool, in Wing et al. [471], pp. 1684-1703.
[109] M. Clavel, F. Durán, N. Martı´-Oliet, Polytypic programming in Maude, in Futatsugi [200], pp. 339-360.; M. Clavel, F. Durán, N. Martı´-Oliet, Polytypic programming in Maude, in Futatsugi [200], pp. 339-360.
[110] M. Clavel, M. Egea, ITP/OCL: a rewriting-based validation tool for UML+OCL static class diagrams, in Johnson and Vene [247], pp. 368-373.; M. Clavel, M. Egea, ITP/OCL: a rewriting-based validation tool for UML+OCL static class diagrams, in Johnson and Vene [247], pp. 368-373.
[111] M. Clavel, S. Eker, P. Lincoln, J. Meseguer, Principles of Maude, in Meseguer [317], pp. 65-89.; M. Clavel, S. Eker, P. Lincoln, J. Meseguer, Principles of Maude, in Meseguer [317], pp. 65-89. · Zbl 0912.68095
[112] M. Clavel, N. Martı´-Oliet, M. Palomino, Formalizing and proving semantic relations between specifications by reflection, in Rattray et al. [389], pp. 72-86.; M. Clavel, N. Martı´-Oliet, M. Palomino, Formalizing and proving semantic relations between specifications by reflection, in Rattray et al. [389], pp. 72-86. · Zbl 1108.68378
[113] M. Clavel, J. Meseguer, Reflection and strategies in rewriting logic, in Meseguer [317], pp. 126-148.; M. Clavel, J. Meseguer, Reflection and strategies in rewriting logic, in Meseguer [317], pp. 126-148. · Zbl 0917.68107
[114] M. Clavel, J. Meseguer, Internal strategies in a reflective logic, in: B. Gramlich, H. Kirchner (Eds.), Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction, Townsville, Australia, 1997, pp. 1-12.; M. Clavel, J. Meseguer, Internal strategies in a reflective logic, in: B. Gramlich, H. Kirchner (Eds.), Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction, Townsville, Australia, 1997, pp. 1-12.
[115] Clavel, M.; Meseguer, J., Reflection in conditional rewriting logic, Theoretical Computer Science, 285, 2, 245-288 (2002) · Zbl 1001.68060
[116] Clavel, M.; Meseguer, J.; Palomino, M., Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Theoretical Computer Science, 373, 1-2, 70-91 (2007) · Zbl 1111.03034
[117] Clavel, M.; Palomino, M.; Riesco, A., Introducing the ITP tool: a tutorial, Journal of Universal Computer Science, 12, 11, 1618-1650 (2006)
[118] M. Clavel, J. Santa-Cruz, ASIP + ITP: a verification tool based on algebraic semantics, in: F.J. López-Fraguas (Ed.), Actas de las V Jornadas sobre Programación y Lenguajes, PROLE 2005, Granada, España, Septiembre 14-16, 2005, Thomson, 2005, pp. 149-158.; M. Clavel, J. Santa-Cruz, ASIP + ITP: a verification tool based on algebraic semantics, in: F.J. López-Fraguas (Ed.), Actas de las V Jornadas sobre Programación y Lenguajes, PROLE 2005, Granada, España, Septiembre 14-16, 2005, Thomson, 2005, pp. 149-158.
[119] W. Clinger, Foundations of actor semantics, Technical report AI-TR-633, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1981.; W. Clinger, Foundations of actor semantics, Technical report AI-TR-633, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1981.
[120] H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree automata techniques and applications, 2007. Available from: <http://www.grappa.univ-lille3.fr/tata; H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree automata techniques and applications, 2007. Available from: <http://www.grappa.univ-lille3.fr/tata
[121] Comon-Lundth, H.; Delaune, S., The finite variant property: how to get rid of some algebraic properties, (Proc RTA’05. Proc RTA’05, LNCS, vol. 3467 (2005), Springer), 294-307 · Zbl 1078.68059
[122] Coquand, T.; Huet, G., The calculus of constructions, Information and Computation, 76, 95-120 (1988) · Zbl 0654.03045
[123] A. Corradini, F. Gadducci, U. Montanari, Relating two categorial models of term rewriting, in Hsiang [243], pp. 225-240.; A. Corradini, F. Gadducci, U. Montanari, Relating two categorial models of term rewriting, in Hsiang [243], pp. 225-240.
[124] A. Corradini, B. Klin, C. Cıˆrstea (Eds.), Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011, Proceedings, Lecture Notes in Computer Science, vol. 6859, Springer, 2011.; A. Corradini, B. Klin, C. Cıˆrstea (Eds.), Algebra and Coalgebra in Computer Science - 4th International Conference, CALCO 2011, Winchester, UK, August 30-September 2, 2011, Proceedings, Lecture Notes in Computer Science, vol. 6859, Springer, 2011.
[125] A. Corradini, U. Montanari (Eds.), Recent Trends in Algebraic Development Techniques, 19th International Workshop, WADT 2008, Pisa, Italy, June 13-16, 2008, Revised Selected Papers, Lecture Notes in Computer Science, vol. 5486, Springer, 2009.; A. Corradini, U. Montanari (Eds.), Recent Trends in Algebraic Development Techniques, 19th International Workshop, WADT 2008, Pisa, Italy, June 13-16, 2008, Revised Selected Papers, Lecture Notes in Computer Science, vol. 5486, Springer, 2009.
[126] de Oliveira, A. S., Rewriting-based access control policies, Electronic Notes in Theoretical Computer Science, 171, 4, 59-72 (2007)
[127] A.S. de Oliveira, E.K. Wang, C. Kirchner, H. Kirchner, Weaving rewrite-based access control policies, in: P. Ning, V. Atluri, V.D. Gligor, H. Mantel (Eds.), Proceedings of the 2007 ACM Workshop on Formal Methods in Security Engineering, FMSE 2007, Fairfax, VA, USA, November 2, 2007, ACM, 2007, pp. 71-80.; A.S. de Oliveira, E.K. Wang, C. Kirchner, H. Kirchner, Weaving rewrite-based access control policies, in: P. Ning, V. Atluri, V.D. Gligor, H. Mantel (Eds.), Proceedings of the 2007 ACM Workshop on Formal Methods in Security Engineering, FMSE 2007, Fairfax, VA, USA, November 2, 2007, ACM, 2007, pp. 71-80.
[128] Degano, P.; Gadducci, F.; Priami, C., A causal semantics for CCS via rewriting logic, Theoretical Computer Science, 275, 1-2, 259-282 (2002) · Zbl 1026.68075
[129] Degano, P.; Meseguer, J.; Montanari, U., Axiomatizing the algebra of net computations and processes, Acta Informatica, 33, 641-667 (1996)
[130] P. Degano, C. Priami, Proved trees, in: Proc. ICALP’92, LNCS, vol. 623, Springer, 1992, pp. 629-640.; P. Degano, C. Priami, Proved trees, in: Proc. ICALP’92, LNCS, vol. 623, Springer, 1992, pp. 629-640.
[131] Denker, G.; Garcı´a-Luna-Aceves, J. J.; Meseguer, J.; Ölveczky, P. C.; Raju, J.; Smith, B.; Talcott, C. L., Specification and analysis of a reliable broadcasting protocol in Maude, (Hajek, B.; Sreenivas, R. S., Proceedings of the 37th Allerton Conference on Communication. Proceedings of the 37th Allerton Conference on Communication, Control and Computation (1999), University of Illinois), 738-747
[132] G. Denker, J. Meseguer, C.L. Talcott, Protocol specification and analysis in Maude, in: N. Heintze, J. Wing (Eds.), Proceedings of the Workshop on Formal Methods and Security Protocols, FMSP’98, Indianapolis, Indiana, June 25, 1998, 1998.; G. Denker, J. Meseguer, C.L. Talcott, Protocol specification and analysis in Maude, in: N. Heintze, J. Wing (Eds.), Proceedings of the Workshop on Formal Methods and Security Protocols, FMSP’98, Indianapolis, Indiana, June 25, 1998, 1998.
[133] G. Denker, J. Meseguer, C.L. Talcott, Formal specification and analysis of active networks and communication protocols: the Maude experience, in Koob et al. [272], pp. 251-265.; G. Denker, J. Meseguer, C.L. Talcott, Formal specification and analysis of active networks and communication protocols: the Maude experience, in Koob et al. [272], pp. 251-265.
[134] G. Denker, J. Meseguer, C.L. Talcott, Rewriting semantics of meta-objects and composable distributed services, in Futatsugi [200], pp. 405-425.; G. Denker, J. Meseguer, C.L. Talcott, Rewriting semantics of meta-objects and composable distributed services, in Futatsugi [200], pp. 405-425. · Zbl 0962.68081
[135] G. Denker, J. Millen, CAPSL and CIL language design: a common authentication protocol specification language and its intermediate language, Technical report SRI-CSL-99-02, Computer Science Laboratory, SRI International, 1999.; G. Denker, J. Millen, CAPSL and CIL language design: a common authentication protocol specification language and its intermediate language, Technical report SRI-CSL-99-02, Computer Science Laboratory, SRI International, 1999.
[136] G. Denker, J. Millen, CAPSL intermediate language, in: N. Heintze, E. Clarke (Eds.), Proceedings of the Workshop on Formal Methods and Security Protocols, FMSP’99, Trento, Italy, July 5, 1999, 1999.; G. Denker, J. Millen, CAPSL intermediate language, in: N. Heintze, E. Clarke (Eds.), Proceedings of the Workshop on Formal Methods and Security Protocols, FMSP’99, Trento, Italy, July 5, 1999, 1999.
[137] G. Denker, J. Millen, CAPSL integrated protocol environment, in Koob et al. [272], pp. 207-222.; G. Denker, J. Millen, CAPSL integrated protocol environment, in Koob et al. [272], pp. 207-222.
[138] G. Denker, J. Millen, The CAPSL integrated protocol environment, Technical report SRI-CSL-2000-02, Computer Science Laboratory, SRI International, 2000.; G. Denker, J. Millen, The CAPSL integrated protocol environment, Technical report SRI-CSL-2000-02, Computer Science Laboratory, SRI International, 2000.
[139] G. Denker, C. Talcott (Eds.), Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1-2, 2006, Electronic Notes in Theoretical Computer Science, vol. 176(4), Elsevier, 2007.; G. Denker, C. Talcott (Eds.), Proceedings of the Sixth International Workshop on Rewriting Logic and its Applications, WRLA 2006, Vienna, Austria, April 1-2, 2006, Electronic Notes in Theoretical Computer Science, vol. 176(4), Elsevier, 2007.
[140] E. Deplagne, C. Kirchner, H. Kirchner, Q.H. Nguyen, Proof search and proof check for equational and inductive theorems, in: F. Baader (Ed.), Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28-August 2, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2741, Springer, 2003, pp. 297-316.; E. Deplagne, C. Kirchner, H. Kirchner, Q.H. Nguyen, Proof search and proof check for equational and inductive theorems, in: F. Baader (Ed.), Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28-August 2, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2741, Springer, 2003, pp. 297-316. · Zbl 1278.68257
[141] R. Diaconescu, K. Futatsugi, CafeOBJ Report. The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, AMAST Series in Computing, vol. 6, World Scientific, 1998.; R. Diaconescu, K. Futatsugi, CafeOBJ Report. The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, AMAST Series in Computing, vol. 6, World Scientific, 1998.
[142] H. Ding, C. Zheng, G. Agha, L. Sha, Automated verification of the dependability of object-oriented real-time systems, in: Proceedings of the 9th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (WORDS 2003 Fall), Anacapri (Capri Island), Italy, October 1-3, 2003, IEEE Computer Society, 2004, pp. 171-178.; H. Ding, C. Zheng, G. Agha, L. Sha, Automated verification of the dependability of object-oriented real-time systems, in: Proceedings of the 9th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (WORDS 2003 Fall), Anacapri (Capri Island), Italy, October 1-3, 2003, IEEE Computer Society, 2004, pp. 171-178.
[143] J.S. Dong, H. Zhu (Eds.), Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6447, Springer, 2010.; J.S. Dong, H. Zhu (Eds.), Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6447, Springer, 2010.
[144] D.J. Dougherty, S. Escobar (Eds.), Proceedings of the Third International Workshop on Security and Rewriting Techniques, SecReT 2008, Pittsburgh, PA, USA, June 22, 2008, Electronic Notes in Theoretical Computer Science, vol. 234, Elsevier, 2009.; D.J. Dougherty, S. Escobar (Eds.), Proceedings of the Third International Workshop on Security and Rewriting Techniques, SecReT 2008, Pittsburgh, PA, USA, June 22, 2008, Electronic Notes in Theoretical Computer Science, vol. 234, Elsevier, 2009.
[145] D.J. Dougherty, C. Kirchner, H. Kirchner, A.S. de Oliveira, Modular access control via strategic rewriting, in: J. Biskup, J. Lopez (Eds.), Computer Security - ESORICS 2007, 12th European Symposium On Research In Computer Security, Dresden, Germany, September 24-26, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4734, Springer, 2007, pp. 578-593.; D.J. Dougherty, C. Kirchner, H. Kirchner, A.S. de Oliveira, Modular access control via strategic rewriting, in: J. Biskup, J. Lopez (Eds.), Computer Security - ESORICS 2007, 12th European Symposium On Research In Computer Security, Dresden, Germany, September 24-26, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4734, Springer, 2007, pp. 578-593.
[146] Dowek, G.; Hardin, T.; Kirchner, C., Higher order unification via explicit substitutions, Information and Computation, 157, 1-2, 183-235 (2000) · Zbl 1005.03016
[147] Dowek, G.; Hardin, T.; Kirchner, C., HOL-\( \lambda \sigma \): an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, 11, 1, 21-45 (2001) · Zbl 0972.03012
[148] Dowek, G.; Hardin, T.; Kirchner, C., Theorem proving modulo, Journal of Automated Reasoning, 31, 1, 33-72 (2003) · Zbl 1049.03011
[149] G. Dowek, C. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, in: B. Klin, P. Sobociński (Eds.), Proceedings of the Sixth Workshop on Structural Operational Semantics, SOS 2009, Bologna, Italy, August 31, 2009, Electronic Proceedings in Theoretical Computer Science, vol. 18, 2010, pp. 77-91.; G. Dowek, C. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, in: B. Klin, P. Sobociński (Eds.), Proceedings of the Sixth Workshop on Structural Operational Semantics, SOS 2009, Bologna, Italy, August 31, 2009, Electronic Proceedings in Theoretical Computer Science, vol. 18, 2010, pp. 77-91.
[150] F. Durán, A Reflective Module Algebra with Applications to the Maude Language, Ph.D. thesis, Universidad de Málaga, Spain, June 1999.; F. Durán, A Reflective Module Algebra with Applications to the Maude Language, Ph.D. thesis, Universidad de Málaga, Spain, June 1999.
[151] F. Durán, The extensibility of Maude’s module algebra, in: T. Rus (Ed.), Algebraic Methodology and Software Technology. 8th International Conference, AMAST 2000, Iowa City, Iowa, USA, May 20-27, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1816,. Springer, 2000, pp. 422-437.; F. Durán, The extensibility of Maude’s module algebra, in: T. Rus (Ed.), Algebraic Methodology and Software Technology. 8th International Conference, AMAST 2000, Iowa City, Iowa, USA, May 20-27, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1816,. Springer, 2000, pp. 422-437.
[152] F. Durán, S. Eker, S. Escobar, J. Meseguer, C.L. Talcott, Variants, unification, narrowing, and symbolic reachability in Maude 2.6, in: M. Schmidt-Schauß (Ed.), Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, Novi Sad, Serbia, May 30-June 1, 2011, Leibniz International Proceedings in Informatics (LIPIcs), vol. 10, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011, pp. 31-40.; F. Durán, S. Eker, S. Escobar, J. Meseguer, C.L. Talcott, Variants, unification, narrowing, and symbolic reachability in Maude 2.6, in: M. Schmidt-Schauß (Ed.), Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, Novi Sad, Serbia, May 30-June 1, 2011, Leibniz International Proceedings in Informatics (LIPIcs), vol. 10, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011, pp. 31-40.
[153] F. Durán, F. Gutiérrez, P. López, E. Pimentel, A formalization of the SMEPP model in Maude, in: V. Cahill (Ed.), Proceedings of the 5th Annual International Conference on Mobile and Ubiquitous Systems: Computing, Networking, and Services, MobiQuitous 2008, July 21-25, 2008, Dublin, Ireland, ACM, 2008.; F. Durán, F. Gutiérrez, P. López, E. Pimentel, A formalization of the SMEPP model in Maude, in: V. Cahill (Ed.), Proceedings of the 5th Annual International Conference on Mobile and Ubiquitous Systems: Computing, Networking, and Services, MobiQuitous 2008, July 21-25, 2008, Dublin, Ireland, ACM, 2008.
[154] F. Durán, J. Herrador, A. Vallecillo, Using UML and Maude for writing and reasoning about ODP policies, in: J. Moffett, F. Garcia (Eds.), Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks, POLICY 2003, Lake Como, Italy, June 4-6, 2003, IEEE Computer Society, 2003, pp. 15-25.; F. Durán, J. Herrador, A. Vallecillo, Using UML and Maude for writing and reasoning about ODP policies, in: J. Moffett, F. Garcia (Eds.), Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks, POLICY 2003, Lake Como, Italy, June 4-6, 2003, IEEE Computer Society, 2003, pp. 15-25.
[155] Durán, F.; Lucas, S.; Marché, C.; Meseguer, J.; Urbain, X., Proving operational termination of membership equational programs, Higher-Order and Symbolic Computation, 21, 1-2, 59-88 (2008) · Zbl 1192.68154
[156] F. Durán, S. Lucas, J. Meseguer, MTT: the Maude termination tool (system description), in: A. Armando, P. Baumgartner, G. Dowek (Eds.), Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5195, Springer, 2008, pp. 313-319.; F. Durán, S. Lucas, J. Meseguer, MTT: the Maude termination tool (system description), in: A. Armando, P. Baumgartner, G. Dowek (Eds.), Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5195, Springer, 2008, pp. 313-319. · Zbl 1165.68360
[157] F. Durán, S. Lucas, J. Meseguer, Methods for proving termination of rewriting-based programming languages by transformation, in: J.M. Almendros-Jiménez (Ed.), Proceedings of the Eighth Spanish Conference on Programming and Computer Languages, PROLE 2008, Gijón, Spain, October 8-10, 2008, Electronic Notes in Theoretical Computer Science, vol. 248, Elsevier, 2009, pp. 93-113.; F. Durán, S. Lucas, J. Meseguer, Methods for proving termination of rewriting-based programming languages by transformation, in: J.M. Almendros-Jiménez (Ed.), Proceedings of the Eighth Spanish Conference on Programming and Computer Languages, PROLE 2008, Gijón, Spain, October 8-10, 2008, Electronic Notes in Theoretical Computer Science, vol. 248, Elsevier, 2009, pp. 93-113. · Zbl 1337.68067
[158] F. Durán, S. Lucas, J. Meseguer, Termination modulo combinations of equational theories, in: S. Ghilardi, R. Sebastiani (Eds.), Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5749, Springer, 2009, pp. 246-262.; F. Durán, S. Lucas, J. Meseguer, Termination modulo combinations of equational theories, in: S. Ghilardi, R. Sebastiani (Eds.), Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5749, Springer, 2009, pp. 246-262. · Zbl 1193.68145
[159] F. Durán, J. Meseguer, An extensible module algebra for Maude, in Kirchner and Kirchner [262], pp. 174-195.; F. Durán, J. Meseguer, An extensible module algebra for Maude, in Kirchner and Kirchner [262], pp. 174-195.
[160] Durán, F.; Meseguer, J., Maude’s module algebra, Science of Computer Programming, 66, 2, 125-153 (2007) · Zbl 1116.68047
[161] F. Durán, J. Meseguer, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Journal of Logic and Algebraic Programming, this volume.; F. Durán, J. Meseguer, On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, Journal of Logic and Algebraic Programming, this volume.
[162] F. Durán, P.C. Ölveczky, A guide to extending Full Maude illustrated with the implementation of Real-Time Maude, in Roşu [403], pp. 83-102.; F. Durán, P.C. Ölveczky, A guide to extending Full Maude illustrated with the implementation of Real-Time Maude, in Roşu [403], pp. 83-102.
[163] F. Durán, M. Ouederni, G. Salaün, Checking protocol compatibility using Maude, in: G. Salaün, M. Sirjani (Eds.), Proceedings of the 8th International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2009, Rhodes, Greece, July 11, 2009, Electronic Notes in Theoretical Computer Science, vol. 255, Elsevier, 2009, pp. 65-81.; F. Durán, M. Ouederni, G. Salaün, Checking protocol compatibility using Maude, in: G. Salaün, M. Sirjani (Eds.), Proceedings of the 8th International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA 2009, Rhodes, Greece, July 11, 2009, Electronic Notes in Theoretical Computer Science, vol. 255, Elsevier, 2009, pp. 65-81. · Zbl 1364.68282
[164] F. Durán, C. Rocha, J.M. Álvarez, Tool interoperability in the Maude formal environment, in Corradini et al. [124], pp. 400-406.; F. Durán, C. Rocha, J.M. Álvarez, Tool interoperability in the Maude formal environment, in Corradini et al. [124], pp. 400-406.
[165] F. Durán, C. Rocha, J.M. Álvarez, Towards a Maude formal environment, in: G. Agha, O. Danvy, J. Meseguer (Eds.), Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, Lecture Notes in Computer Science, vol. 7000, Springer, 2011, pp. 329-351.; F. Durán, C. Rocha, J.M. Álvarez, Towards a Maude formal environment, in: G. Agha, O. Danvy, J. Meseguer (Eds.), Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, Lecture Notes in Computer Science, vol. 7000, Springer, 2011, pp. 329-351.
[166] Durán, F.; Roldán, M.; Vallecillo, A., Using Maude to write and execute ODP information viewpoint specifications, Computer Standards & Interfaces, 27, 6, 597-620 (2005)
[167] F. Durán, A. Vallecillo, Specifying the ODP information viewpoint using Maude, in: H. Kilov, K. Baclawski (Eds.), Proceedings of the Tenth OOPSLA Workshop on Behavioral Semantics, Tampa Bay, Florida, October 2001, pp. 44-57.; F. Durán, A. Vallecillo, Specifying the ODP information viewpoint using Maude, in: H. Kilov, K. Baclawski (Eds.), Proceedings of the Tenth OOPSLA Workshop on Behavioral Semantics, Tampa Bay, Florida, October 2001, pp. 44-57.
[168] Durán, F.; Vallecillo, A., Formalizing ODP enterprise specifications in Maude, Computer Standards & Interfaces, 25, 2, 83-102 (2003)
[169] Egea, M.; Rusu, V., Formal executable semantics for conformance in the MDE framework, Innovations in Systems and Software Engineering, 6, 1-2, 73-81 (2009)
[170] Eker, J.; Janneck, J. W.; Lee, E. A.; Liu, J.; Liu, X.; Ludvig, J.; Neuendorffer, S.; Sachs, S.; Xiong, Y., Taming heterogeneity – the Ptolemy approach, Proceedings of the IEEE, 91, 1, 127-144 (2003)
[171] S. Eker, Fast matching in combination of regular equational theories, in Meseguer [317], pp. 90-109.; S. Eker, Fast matching in combination of regular equational theories, in Meseguer [317], pp. 90-109.
[172] S. Eker, Associative-commutative rewriting on large terms, in Nieuwenhuis [355], pp. 14-29.; S. Eker, Associative-commutative rewriting on large terms, in Nieuwenhuis [355], pp. 14-29. · Zbl 1038.68560
[173] S. Eker, M. Knapp, K. Laderoute, P. Lincoln, J. Meseguer, M.K. Sönmez, Pathway logic: symbolic analysis of biological signaling, in: R.B. Altman, A.K. Dunker, L. Hunter, T.E. Klein (Eds.), Proceedings of the 7th Pacific Symposium on Biocomputing, PSB 2002, Lihue, Hawaii, USA, January 3-7, 2002, January 2002, pp. 400-412.; S. Eker, M. Knapp, K. Laderoute, P. Lincoln, J. Meseguer, M.K. Sönmez, Pathway logic: symbolic analysis of biological signaling, in: R.B. Altman, A.K. Dunker, L. Hunter, T.E. Klein (Eds.), Proceedings of the 7th Pacific Symposium on Biocomputing, PSB 2002, Lihue, Hawaii, USA, January 3-7, 2002, January 2002, pp. 400-412.
[174] S. Eker, M. Knapp, K. Laderoute, P. Lincoln, C. Talcott, Pathway logic: executable models of biological networks, in Gadducci and Montanari [205], pp. 144-161.; S. Eker, M. Knapp, K. Laderoute, P. Lincoln, C. Talcott, Pathway logic: executable models of biological networks, in Gadducci and Montanari [205], pp. 144-161.
[175] S. Eker, N. Martı´-Oliet, J. Meseguer, A. Verdejo, Deduction, strategies, and rewriting, in: M. Archer, T.B. de la Tour, C. Muñoz (Eds.), Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006, Seattle, WA, USA, August 16, 2006, Electronic Notes in Theoretical Computer Science, vol. 174(11), Elsevier, 2007, pp. 3-25.; S. Eker, N. Martı´-Oliet, J. Meseguer, A. Verdejo, Deduction, strategies, and rewriting, in: M. Archer, T.B. de la Tour, C. Muñoz (Eds.), Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006, Seattle, WA, USA, August 16, 2006, Electronic Notes in Theoretical Computer Science, vol. 174(11), Elsevier, 2007, pp. 3-25. · Zbl 1277.68241
[176] C. Ellison, G. Roşu, A formal semantics of C with applications, Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, 2010.; C. Ellison, G. Roşu, A formal semantics of C with applications, Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, 2010.
[177] C. Ellison, T.F. Şerbănuţă, G. Roşu, A rewriting logic approach to type inference, in Corradini and Montanari [125], pp. 135-151.; C. Ellison, T.F. Şerbănuţă, G. Roşu, A rewriting logic approach to type inference, in Corradini and Montanari [125], pp. 135-151. · Zbl 1253.68211
[178] S. Escobar, J. Hendrix, C. Meadows, J. Meseguer, Diffie-Hellman cryptographic reasoning in the Maude-NRL Protocol Analyzer, in: M. Nesi, R. Treinen (Eds.), Proceedings of the Second International Workshop on Security and Rewriting Techniques, SecReT 2007, Paris, France, June 29, 2007, 2007.; S. Escobar, J. Hendrix, C. Meadows, J. Meseguer, Diffie-Hellman cryptographic reasoning in the Maude-NRL Protocol Analyzer, in: M. Nesi, R. Treinen (Eds.), Proceedings of the Second International Workshop on Security and Rewriting Techniques, SecReT 2007, Paris, France, June 29, 2007, 2007.
[179] S. Escobar, D. Kapur, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, R. Sasse. Protocol analysis in Maude-NPA using unification modulo homomorphic encryption, in Schneider-Kamp and Hanus [416], pp. 65-76.; S. Escobar, D. Kapur, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, R. Sasse. Protocol analysis in Maude-NPA using unification modulo homomorphic encryption, in Schneider-Kamp and Hanus [416], pp. 65-76.
[180] Escobar, S.; Meadows, C.; Meseguer, J., A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties, Theoretical Computer Science, 367, 1-2, 162-202 (2006) · Zbl 1153.94375
[181] S. Escobar, C. Meadows, J. Meseguer, Equational cryptographic reasoning in the Maude-NRL Protocol Analyzer, in: M. Fernández, C. Kirchner (Eds.), Proceedings of the First International Workshop on Security and Rewriting Techniques, SecReT 2006, Venice, Italy, July 15, 2006, Electronic Notes in Theoretical Computer Science, vol. 171(4), Elsevier, 2007, pp. 23-36.; S. Escobar, C. Meadows, J. Meseguer, Equational cryptographic reasoning in the Maude-NRL Protocol Analyzer, in: M. Fernández, C. Kirchner (Eds.), Proceedings of the First International Workshop on Security and Rewriting Techniques, SecReT 2006, Venice, Italy, July 15, 2006, Electronic Notes in Theoretical Computer Science, vol. 171(4), Elsevier, 2007, pp. 23-36.
[182] S. Escobar, C. Meadows, J. Meseguer, State space reduction in the Maude-NRL Protocol Analyzer, in: S. Jajodia, J. López (Eds.), Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security, Málaga, Spain, October 6-8, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5283, Springer, 2008, pp. 548-562.; S. Escobar, C. Meadows, J. Meseguer, State space reduction in the Maude-NRL Protocol Analyzer, in: S. Jajodia, J. López (Eds.), Computer Security - ESORICS 2008, 13th European Symposium on Research in Computer Security, Málaga, Spain, October 6-8, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5283, Springer, 2008, pp. 548-562. · Zbl 1360.94307
[183] S. Escobar, C. Meadows, J. Meseguer, Maude-NPA: cryptographic protocol analysis modulo equational properties, in: A. Aldini, G. Barthe, R. Gorrieri (Eds.), Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, Lecture Notes in Computer Science, vol. 5705, Springer, 2009, pp. 1-50.; S. Escobar, C. Meadows, J. Meseguer, Maude-NPA: cryptographic protocol analysis modulo equational properties, in: A. Aldini, G. Barthe, R. Gorrieri (Eds.), Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures, Lecture Notes in Computer Science, vol. 5705, Springer, 2009, pp. 1-50. · Zbl 1252.94061
[184] S. Escobar, C. Meadows, J. Meseguer, State space reduction in the Maude-NRL protocol analyzer, May 2011. Available from: <http://arxiv.org/abs/1105.5282>; S. Escobar, C. Meadows, J. Meseguer, State space reduction in the Maude-NRL protocol analyzer, May 2011. Available from: <http://arxiv.org/abs/1105.5282> · Zbl 1360.94307
[185] S. Escobar, C. Meadows, J. Meseguer, S. Santiago, Sequential protocol composition in Maude-NPA, in: D. Gritzalis, B. Preneel, M. Theoharidou (Eds.), Computer Security - ESORICS 2010, 15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6345, Springer, 2010, pp. 303-318.; S. Escobar, C. Meadows, J. Meseguer, S. Santiago, Sequential protocol composition in Maude-NPA, in: D. Gritzalis, B. Preneel, M. Theoharidou (Eds.), Computer Security - ESORICS 2010, 15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6345, Springer, 2010, pp. 303-318.
[186] S. Escobar, J. Meseguer, Symbolic model checking of infinite-state systems using narrowing, in Baader [35], pp. 153-168.; S. Escobar, J. Meseguer, Symbolic model checking of infinite-state systems using narrowing, in Baader [35], pp. 153-168. · Zbl 1203.68097
[187] S. Escobar, J. Meseguer, R. Sasse, Effectively checking the finite variant property, in: A. Voronkov (Ed.), Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5117, Springer, 2008, pp. 79-93.; S. Escobar, J. Meseguer, R. Sasse, Effectively checking the finite variant property, in: A. Voronkov (Ed.), Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5117, Springer, 2008, pp. 79-93. · Zbl 1145.68444
[188] S. Escobar, J. Meseguer, P. Thati, Narrowing and rewriting logic: from foundations to applications, in: F.J. López-Fraguas (Ed.), Proceedings of the 15th Workshop on Functional and (Constraint) Logic Programming, WFLP 2006, Madrid, Spain, November 16-17, 2006, Electronic Notes in Theoretical Computer Science, vol. 177, Elsevier, 2007, pp. 5-33.; S. Escobar, J. Meseguer, P. Thati, Narrowing and rewriting logic: from foundations to applications, in: F.J. López-Fraguas (Ed.), Proceedings of the 15th Workshop on Functional and (Constraint) Logic Programming, WFLP 2006, Madrid, Spain, November 16-17, 2006, Electronic Notes in Theoretical Computer Science, vol. 177, Elsevier, 2007, pp. 5-33. · Zbl 1279.68205
[189] S. Escobar, R. Sasse, J. Meseguer, Folding variant narrowing and optimal variant termination, in Ölveczky [362], pp. 52-68.; S. Escobar, R. Sasse, J. Meseguer, Folding variant narrowing and optimal variant termination, in Ölveczky [362], pp. 52-68. · Zbl 1306.68069
[190] S. Escobar, R. Sasse, J. Meseguer, Folding variant narrowing and optimal variant termination, Journal of Logic and Algebraic Programming, this volume.; S. Escobar, R. Sasse, J. Meseguer, Folding variant narrowing and optimal variant termination, Journal of Logic and Algebraic Programming, this volume. · Zbl 1306.68069
[191] A. Farzan, F. Chen, J. Meseguer, G. Roşu, Formal analysis of Java programs in JavaFAN, in: R. Alur, D. Peled (Eds.), Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3114, Springer, 2004, pp. 501-505.; A. Farzan, F. Chen, J. Meseguer, G. Roşu, Formal analysis of Java programs in JavaFAN, in: R. Alur, D. Peled (Eds.), Computer Aided Verification, 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3114, Springer, 2004, pp. 501-505. · Zbl 1103.68611
[192] A. Farzan, J. Meseguer, State space reduction of rewrite theories using invisible transitions, in Johnson and Vene [247], pp. 142-157.; A. Farzan, J. Meseguer, State space reduction of rewrite theories using invisible transitions, in Johnson and Vene [247], pp. 142-157. · Zbl 1236.68182
[193] A. Farzan, J. Meseguer, Partial order reduction for rewriting semantics of programming languages, in Denker and Talcott [139], pp. 61-78.; A. Farzan, J. Meseguer, Partial order reduction for rewriting semantics of programming languages, in Denker and Talcott [139], pp. 61-78. · Zbl 1279.68207
[194] A. Farzan, J. Meseguer, G. Roşu, Formal JVM code analysis in JavaFAN, in Rattray et al. [389], pp. 132-147.; A. Farzan, J. Meseguer, G. Roşu, Formal JVM code analysis in JavaFAN, in Rattray et al. [389], pp. 132-147. · Zbl 1108.68382
[195] Feferman, S., Finitary inductively presented logics, (Ferro, R.; etal., Logic Colloquium’88 (1989), North-Holland), 191-220 · Zbl 0823.03032
[196] A. Felty, D. Miller, Encoding a dependent-type \(\operatorname{\Lambda;} \); A. Felty, D. Miller, Encoding a dependent-type \(\operatorname{\Lambda;} \) · Zbl 0708.68090
[197] J.L. Fernández Alemán, J.A. Toval Álvarez, Can intuition become rigorous? Foundations for UML model verification tools, in: F.M. Titsworth (Ed.), Proceedings of the 11th International Symposium on Software Reliability Engineering, ISSRE 2000, San Jose, CA, USA, October 8-11, 2000, IEEE Computer Society, 2000, pp. 344-355.; J.L. Fernández Alemán, J.A. Toval Álvarez, Can intuition become rigorous? Foundations for UML model verification tools, in: F.M. Titsworth (Ed.), Proceedings of the 11th International Symposium on Software Reliability Engineering, ISSRE 2000, San Jose, CA, USA, October 8-11, 2000, IEEE Computer Society, 2000, pp. 344-355.
[198] O. Fissore, I. Gnaedig, H. Kirchner, System presentation - CARIBOO: an induction based proof tool for termination with strategies, in: C. Kirchner (Ed.), Proceedings of the 4th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2002, Pittsburgh, PA, USA, October 6-8, 2002 (affiliated with PLI 2002), ACM, 2002, pp. 62-73.; O. Fissore, I. Gnaedig, H. Kirchner, System presentation - CARIBOO: an induction based proof tool for termination with strategies, in: C. Kirchner (Ed.), Proceedings of the 4th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2002, Pittsburgh, PA, USA, October 6-8, 2002 (affiliated with PLI 2002), ACM, 2002, pp. 62-73.
[199] O. Fissore, I. Gnaedig, H. Kirchner, Simplification and termination of strategies in rule-based languages, in: D. Miller, K. Sagonas (Eds.), Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2003, Uppsala, Sweden, August 27-29, 2003, ACM, 2003, pp. 124-135.; O. Fissore, I. Gnaedig, H. Kirchner, Simplification and termination of strategies in rule-based languages, in: D. Miller, K. Sagonas (Eds.), Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2003, Uppsala, Sweden, August 27-29, 2003, ACM, 2003, pp. 124-135.
[200] K. Futatsugi (Ed.), Proceedings of the Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000, Electronic Notes in Theoretical Computer Science, vol. 36, Elsevier, 2000.; K. Futatsugi (Ed.), Proceedings of the Third International Workshop on Rewriting Logic and its Applications, WRLA 2000, Kanazawa, Japan, September 18-20, 2000, Electronic Notes in Theoretical Computer Science, vol. 36, Elsevier, 2000.
[201] K. Futatsugi, Verifying specifications with proof scores in CafeOBJ, in: S. Uchitel, S. Easterbrook (Eds.), Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006, Tokyo, Japan, September 18-22, 2006, IEEE Computer Society, 2006, pp. 3-10.; K. Futatsugi, Verifying specifications with proof scores in CafeOBJ, in: S. Uchitel, S. Easterbrook (Eds.), Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006, Tokyo, Japan, September 18-22, 2006, IEEE Computer Society, 2006, pp. 3-10.
[202] K. Futatsugi, Fostering proof scores in CafeOBJ, in Dong and Zhu [143], pp. 1-20.; K. Futatsugi, Fostering proof scores in CafeOBJ, in Dong and Zhu [143], pp. 1-20. · Zbl 1019.68523
[203] (Futatsugi, K.; Nakagawa, A. T.; Tamai, T., Cafe: An Industrial-Strength Algebraic Formal Method (2000), Elsevier)
[204] Gabbay, D. M.; Pnueli, A., A sound and complete deductive system for CTL* verification, Logic Journal of the IGPL, 16, 6, 499-536 (2008) · Zbl 1156.68036
[205] F. Gadducci, U. Montanari (Eds.), Proceedings of the Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, Electronic Notes in Theoretical Computer Science, vol. 71, Elsevier, 2004.; F. Gadducci, U. Montanari (Eds.), Proceedings of the Fourth International Workshop on Rewriting Logic and its Applications, WRLA 2002, Pisa, Italy, September 19-21, 2002, Electronic Notes in Theoretical Computer Science, vol. 71, Elsevier, 2004.
[206] P. Gardner, Representing Logics in Type Theory, Ph.D. thesis, Technical report CST-93-92, Department of Computer Science, University of Edinburgh, 1992.; P. Gardner, Representing Logics in Type Theory, Ph.D. thesis, Technical report CST-93-92, Department of Computer Science, University of Edinburgh, 1992.
[207] A. Garrido, J. Meseguer, Formal specification and verification of Java refactorings, in: Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006, Philadelphia, Pennsylvania, September 27-29, 2006, IEEE, 2006, pp. 165-174.; A. Garrido, J. Meseguer, Formal specification and verification of Java refactorings, in: Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation, SCAM 2006, Philadelphia, Pennsylvania, September 27-29, 2006, IEEE, 2006, pp. 165-174.
[208] A. Garrido, J. Meseguer, R. Johnson, Algebraic semantics of the C preprocessor and correctness of its refactorings, Technical report UIUCDCS-R-2006-2688, Department of Computer Science, University of Illinois at Urbana-Champaign, February 2006.; A. Garrido, J. Meseguer, R. Johnson, Algebraic semantics of the C preprocessor and correctness of its refactorings, Technical report UIUCDCS-R-2006-2688, Department of Computer Science, University of Illinois at Urbana-Champaign, February 2006.
[209] J. Giesl (Ed.), Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3467, Springer, 2005.; J. Giesl (Ed.), Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3467, Springer, 2005.
[210] Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S., Automated termination proofs with AProVE, (RTA 2004. RTA 2004, LNCS, vol. 3091 (2004), Springer), 210-220
[211] P. Glynn, The role of generalized semi-Markov processes in simulation output analysis, 1983.; P. Glynn, The role of generalized semi-Markov processes in simulation output analysis, 1983.
[212] I. Gnaedig, Induction for positive almost sure termination, in Leuschel and Podelski [284], pp. 167-178.; I. Gnaedig, Induction for positive almost sure termination, in Leuschel and Podelski [284], pp. 167-178.
[213] I. Gnaedig, H. Kirchner, Computing constructor forms with non terminating rewrite programs, in: A. Bossi, M.J. Maher (Eds.), Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2006, Venice, Italy, July 10-12, 2006, ACM, 2006, pp. 121-132.; I. Gnaedig, H. Kirchner, Computing constructor forms with non terminating rewrite programs, in: A. Bossi, M.J. Maher (Eds.), Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2006, Venice, Italy, July 10-12, 2006, ACM, 2006, pp. 121-132.
[214] Gnaedig, I.; Kirchner, H., Termination of rewriting under strategies, ACM Transactions on Computational Logic, 10, 2 (2009) · Zbl 1351.68129
[215] Goguen, J., OBJ as a theorem prover with application to hardware verification, (Subramanyam, P.; Birtwistle, G., Current Trends in Hardware Verification and Automated Theorem Proving (1989), Springer Verlag), 218-267
[216] Goguen, J.; Burstall, R., Institutions: abstract model theory for specification and programming, Journal of the ACM, 39, 1, 95-146 (1992) · Zbl 0799.68134
[217] J. Goguen, J. Meseguer, Security policies and security models, in: Proceedings of the 1982 Symposium on Security and Privacy, IEEE, 1982, pp. 11-20.; J. Goguen, J. Meseguer, Security policies and security models, in: Proceedings of the 1982 Symposium on Security and Privacy, IEEE, 1982, pp. 11-20.
[218] Goguen, J.; Winkler, T.; Meseguer, J.; Futatsugi, K.; Jouannaud, J.-P., Introducing OBJ, (Software Engineering with OBJ: Algebraic Specification in Action (2000), Kluwer), 3-167
[219] Goguen, J. A.; Stevens, A.; Hobley, K.; Hilberdink, H., 2OBJ: a meta-logical framework based on equational logic, Philosophical Transactions of the Royal Society, Series A, 339, 69-86 (1992)
[220] A. Goodloe, Private communication, May 25, 2011.; A. Goodloe, Private communication, May 25, 2011.
[221] A. Goodloe, C.A. Gunter, M.-O. Stehr, Formal prototyping in early stages of protocol design, in: C. Meadows (Ed.), Proceedings of the POPL 2005 Workshop on Issues in the Theory of Security, WITS 2005, Long Beach, California, USA, January 10-11, 2005, ACM, 2005, pp. 67-80.; A. Goodloe, C.A. Gunter, M.-O. Stehr, Formal prototyping in early stages of protocol design, in: C. Meadows (Ed.), Proceedings of the POPL 2005 Workshop on Issues in the Theory of Security, WITS 2005, Long Beach, California, USA, January 10-11, 2005, ACM, 2005, pp. 67-80.
[222] A. Goodloe, M. Jacobs, G. Shah, C. Gunter, L3A: a protocol for layer three accounting, in: Proceedings of the First Workshop on Secure Network Protocols, NPSEC 2005, Boston, Massachusetts, November 6, 2005, IEEE Computer Society, 2005, pp. 1-6.; A. Goodloe, M. Jacobs, G. Shah, C. Gunter, L3A: a protocol for layer three accounting, in: Proceedings of the First Workshop on Secure Network Protocols, NPSEC 2005, Boston, Massachusetts, November 6, 2005, IEEE Computer Society, 2005, pp. 1-6.
[223] A. Goodloe, M. McDougall, C.A. Gunter, M.-O. Stehr, Design and analysis of Sectrace: a protocol to set up security associations and policies in ipsec networks, Technical report, CIS Department, University of Pennsylvania, 2004. Available from: <http://seclab.web.cs.illinois.edu/penn-security-lab>; A. Goodloe, M. McDougall, C.A. Gunter, M.-O. Stehr, Design and analysis of Sectrace: a protocol to set up security associations and policies in ipsec networks, Technical report, CIS Department, University of Pennsylvania, 2004. Available from: <http://seclab.web.cs.illinois.edu/penn-security-lab>
[224] C. Grier, S. Tang, S.T. King, Secure web browsing with the OP web browser, in: 2008 IEEE Symposium on Security and Privacy (S&P 2008), Oakland, California, May 18-21, 2008, IEEE Computer Society, 2008, pp. 402-416.; C. Grier, S. Tang, S.T. King, Secure web browsing with the OP web browser, in: 2008 IEEE Symposium on Security and Privacy (S&P 2008), Oakland, California, May 18-21, 2008, IEEE Computer Society, 2008, pp. 402-416.
[225] R. Gutiérrez, S. Lucas, Proving termination in the context-sensitive dependency pair framework, in Ölveczky [362], pp. 18-34.; R. Gutiérrez, S. Lucas, Proving termination in the context-sensitive dependency pair framework, in Ölveczky [362], pp. 18-34.
[226] S. Gutierrez-Nolasco, N. Venkatasubramanian, M.-O. Stehr, C.L. Talcott, Exploring adaptability of secure group communication using formal prototyping techniques, in: F. Kon, F.M. Costa, N. Wang, R. Cerqueira (Eds.), Proceedings of the 3rd Workshop on Adaptive and Reflective Middleware, Toronto, Ontario, Canada, October 19, 2004, ACM, 2004, pp. 232-237.; S. Gutierrez-Nolasco, N. Venkatasubramanian, M.-O. Stehr, C.L. Talcott, Exploring adaptability of secure group communication using formal prototyping techniques, in: F. Kon, F.M. Costa, N. Wang, R. Cerqueira (Eds.), Proceedings of the 3rd Workshop on Adaptive and Reflective Middleware, Toronto, Ontario, Canada, October 19, 2004, ACM, 2004, pp. 232-237.
[227] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects of Computing, 6, 5, 512-535 (1994) · Zbl 0820.68113
[228] N.A. Harman, Correctness and verification of hardware systems using Maude, Technical report 3-2000, Department of Computer Science, University of Wales Swansea, 2000.; N.A. Harman, Correctness and verification of hardware systems using Maude, Technical report 3-2000, Department of Computer Science, University of Wales Swansea, 2000.
[229] N.A. Harman, Verifying a simple pipelined microprocessor using Maude, in: M. Cerioli, G. Reggio (Eds.), Recent Trends in Algebraic Development Techniques, 15th International Workshop, WADT 2001, Joint with the CoFI WG Meeting, Genova, Italy, April 1-3, 2001, Selected Papers, Lecture Notes in Computer Science, vol. 2267, Springer, 2001, pp. 128-151.; N.A. Harman, Verifying a simple pipelined microprocessor using Maude, in: M. Cerioli, G. Reggio (Eds.), Recent Trends in Algebraic Development Techniques, 15th International Workshop, WADT 2001, Joint with the CoFI WG Meeting, Genova, Italy, April 1-3, 2001, Selected Papers, Lecture Notes in Computer Science, vol. 2267, Springer, 2001, pp. 128-151. · Zbl 1043.68571
[230] Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, Journal of the Association Computing Machinery, 40, 1, 143-184 (1993) · Zbl 0778.03004
[231] J. Hendrix, Decision Procedures for Equationally Based Reasoning, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, 2008. Available from: <http://hdl.handle.net/2142/10967>; J. Hendrix, Decision Procedures for Equationally Based Reasoning, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, 2008. Available from: <http://hdl.handle.net/2142/10967>
[232] J. Hendrix, M. Clavel, J. Meseguer, A sufficient completeness reasoning tool for partial specifications, in Giesl [209], pp. 165-174.; J. Hendrix, M. Clavel, J. Meseguer, A sufficient completeness reasoning tool for partial specifications, in Giesl [209], pp. 165-174. · Zbl 1078.68668
[233] J. Hendrix, D. Kapur, J. Meseguer, Coverset induction with partiality and subsorts: a powerlist case study, in: M. Kaufmann, L.C. Paulson (Eds.), Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6172, Springer, 2010, pp. 275-290.; J. Hendrix, D. Kapur, J. Meseguer, Coverset induction with partiality and subsorts: a powerlist case study, in: M. Kaufmann, L.C. Paulson (Eds.), Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6172, Springer, 2010, pp. 275-290. · Zbl 1291.68346
[234] J. Hendrix, J. Meseguer, On the completeness of context-sensitive order-sorted specifications, in Baader [35], pp. 229-245.; J. Hendrix, J. Meseguer, On the completeness of context-sensitive order-sorted specifications, in Baader [35], pp. 229-245. · Zbl 1203.68098
[235] J. Hendrix, J. Meseguer, Order-sorted equational unification revisited, in Kniesel and Pinto [270], pp. 16-29.; J. Hendrix, J. Meseguer, Order-sorted equational unification revisited, in Kniesel and Pinto [270], pp. 16-29. · Zbl 1291.68220
[236] J. Hendrix, J. Meseguer, H. Ohsaki, A sufficient completeness checker for linear order-sorted specifications modulo axioms, in: U. Furbach, N. Shankar (Eds.), Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4130, Springer, 2006, pp. 151-155.; J. Hendrix, J. Meseguer, H. Ohsaki, A sufficient completeness checker for linear order-sorted specifications modulo axioms, in: U. Furbach, N. Shankar (Eds.), Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4130, Springer, 2006, pp. 151-155.
[237] J. Hendrix, H. Ohsaki, J. Meseguer, Sufficient completeness checking with propositional tree automata, Technical report UIUCDCS-R-2005-2635, Department of Computer Science, University of Illinois at Urbana-Champaign, 2005.; J. Hendrix, H. Ohsaki, J. Meseguer, Sufficient completeness checking with propositional tree automata, Technical report UIUCDCS-R-2005-2635, Department of Computer Science, University of Illinois at Urbana-Champaign, 2005.
[238] J. Hendrix, H. Ohsaki, M. Viswanathan, Propositional tree automata, in: F. Pfenning (Ed.), Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4098, Springer, 2006, pp. 50-65.; J. Hendrix, H. Ohsaki, M. Viswanathan, Propositional tree automata, in: F. Pfenning (Ed.), Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4098, Springer, 2006, pp. 50-65. · Zbl 1151.68460
[239] M. Hills, T.B. Aktemur, G. Roşu, An executable semantic definition of the Beta language using rewriting logic, Technical report UIUCDCS-R-2005-2650, Department of Computer Science, University of Illinois at Urbana-Champaign, 2005.; M. Hills, T.B. Aktemur, G. Roşu, An executable semantic definition of the Beta language using rewriting logic, Technical report UIUCDCS-R-2005-2650, Department of Computer Science, University of Illinois at Urbana-Champaign, 2005.
[240] M. Hills, F. Chen, G. Roşu, A rewriting logic approach to static checking of units of measurement in C, in Kniesel and Pinto [270], pp. 76-91.; M. Hills, F. Chen, G. Roşu, A rewriting logic approach to static checking of units of measurement in C, in Kniesel and Pinto [270], pp. 76-91.
[241] M. Hills, G. Roşu, KOOL: an application of rewriting logic to language prototyping and analysis, in Baader [35], pp. 246-256.; M. Hills, G. Roşu, KOOL: an application of rewriting logic to language prototyping and analysis, in Baader [35], pp. 246-256.
[242] M.M. Hölzl, M. Meier, M. Wirsing, Which soft constraints do you prefer? In Roşu [403], pp. 189-205.; M.M. Hölzl, M. Meier, M. Wirsing, Which soft constraints do you prefer? In Roşu [403], pp. 189-205. · Zbl 1347.68197
[243] J. Hsiang (Ed.), Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, Lecture Notes in Computer Science, vol. 914, Springer, 1995.; J. Hsiang (Ed.), Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings, Lecture Notes in Computer Science, vol. 914, Springer, 1995.
[244] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, Journal of the Association for Computing Machinery, 27, 797-821 (1980) · Zbl 0458.68007
[245] E.B. Johnsen, O. Owe, E.W. Axelsen, A run-time environment for concurrent objects with asynchronous method calls, in Martı´-Oliet [297], pp. 375-392.; E.B. Johnsen, O. Owe, E.W. Axelsen, A run-time environment for concurrent objects with asynchronous method calls, in Martı´-Oliet [297], pp. 375-392. · Zbl 1272.68186
[246] M. Johnson, D. Pavlovic (Eds.), Algebraic Methodology and Software Technology, 13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6486, Springer, 2011.; M. Johnson, D. Pavlovic (Eds.), Algebraic Methodology and Software Technology, 13th International Conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23-25, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6486, Springer, 2011.
[247] M. Johnson, V. Vene (Eds.), Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Kuressaare, Estonia, July 5-8, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4019, Springer, 2006.; M. Johnson, V. Vene (Eds.), Algebraic Methodology and Software Technology, 11th International Conference, AMAST 2006, Kuressaare, Estonia, July 5-8, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4019, Springer, 2006.
[248] Jouannaud, J.-P.; Kirchner, Hélène, Completion of a set of rules modulo a set of equations, SIAM Journal of Computing, 15, 1155-1194 (1986) · Zbl 0665.03005
[249] Jouannaud, J.-P.; Kirchner, C.; Kirchner, H., Incremental construction of unification algorithms in equational theories, (Proc. ICALP’83. Proc. ICALP’83, LNCS, vol. 154 (1983), Springer), 361-373
[250] Kapur, D.; Subramaniam, M., Mechanical verification of adder circuits using rewrite rule laboratory, Formal Methods in System Design, 13, 2, 127-158 (1998)
[251] M. Katelman, A Meta-Language for Functional Verification, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, 2011. Available from: <http://hdl.handle.net/2142/29614>; M. Katelman, A Meta-Language for Functional Verification, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, 2011. Available from: <http://hdl.handle.net/2142/29614>
[252] M. Katelman, S. Keller, J. Meseguer, Concurrent rewriting semantics and analysis of asynchronous digital circuits, in Ölveczky [362], pp. 140-156.; M. Katelman, S. Keller, J. Meseguer, Concurrent rewriting semantics and analysis of asynchronous digital circuits, in Ölveczky [362], pp. 140-156. · Zbl 1306.68078
[253] M. Katelman, S. Keller, J. Meseguer, Rewriting semantics of production rule sets, Journal of Logic and Algebraic Programming, this volume.; M. Katelman, S. Keller, J. Meseguer, Rewriting semantics of production rule sets, Journal of Logic and Algebraic Programming, this volume. · Zbl 1279.68188
[254] M. Katelman, J. Meseguer, A rewriting semantics for ABEL with applications to hardware/software co-design and analysis, in Denker and Talcott [139], pp. 47-60.; M. Katelman, J. Meseguer, A rewriting semantics for ABEL with applications to hardware/software co-design and analysis, in Denker and Talcott [139], pp. 47-60. · Zbl 1279.68189
[255] M. Katelman, J. Meseguer, Using the PALS architecture to verify a distributed topology control protocol for wireless multi-hop networks in the presence of node failures, in Ölveczky [361], pp. 101-116.; M. Katelman, J. Meseguer, Using the PALS architecture to verify a distributed topology control protocol for wireless multi-hop networks in the presence of node failures, in Ölveczky [361], pp. 101-116.
[256] M. Katelman, J. Meseguer, vlogsl: a strategy language for simulation-based verification of hardware, in: S. Barner, I.G. Harris, D. Kroening, O. Raz (Eds.), Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers, Lecture Notes in Computer Science, vol. 6504, Springer, 2011, pp. 129-145.; M. Katelman, J. Meseguer, vlogsl: a strategy language for simulation-based verification of hardware, in: S. Barner, I.G. Harris, D. Kroening, O. Raz (Eds.), Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers, Lecture Notes in Computer Science, vol. 6504, Springer, 2011, pp. 129-145. · Zbl 1325.68150
[257] M. Katelman, J. Meseguer, S. Escobar, Directed-logical testing for functional verification of microprocessors, in: S.A. Edwards, K. Schneider (Eds.), Proceedings of the 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2008, Anaheim, CA, USA, June 5-7, 2008, IEEE Computer Society, 2008, pp. 89-100.; M. Katelman, J. Meseguer, S. Escobar, Directed-logical testing for functional verification of microprocessors, in: S.A. Edwards, K. Schneider (Eds.), Proceedings of the 6th ACM & IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE 2008, Anaheim, CA, USA, June 5-7, 2008, IEEE Computer Society, 2008, pp. 89-100.
[258] M. Katelman, J. Meseguer, J.C. Hou, Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking, in Barthe and de Boer [49], pp. 150-169.; M. Katelman, J. Meseguer, J.C. Hou, Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking, in Barthe and de Boer [49], pp. 150-169.
[259] M. Kim, M.-O. Stehr, C.L. Talcott, N. Dutt, N. Venkatasubramanian, Combining formal verification with observed system execution behavior to tune system parameters, in: J.-F. Raskin, P.S. Thiagarajan (Eds.), Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4763, Springer, 2007, pp. 257-273.; M. Kim, M.-O. Stehr, C.L. Talcott, N. Dutt, N. Venkatasubramanian, Combining formal verification with observed system execution behavior to tune system parameters, in: J.-F. Raskin, P.S. Thiagarajan (Eds.), Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4763, Springer, 2007, pp. 257-273.
[260] M. Kim, M.-O. Stehr, C.L. Talcott, N. Dutt, N. Venkatasubramanian, Constraint refinement for online verifiable cross-layer system adaptation, in: Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008, IEEE, 2008, pp. 646-651.; M. Kim, M.-O. Stehr, C.L. Talcott, N. Dutt, N. Venkatasubramanian, Constraint refinement for online verifiable cross-layer system adaptation, in: Design, Automation and Test in Europe, DATE 2008, Munich, Germany, March 10-14, 2008, IEEE, 2008, pp. 646-651.
[261] M. Kim, M.-O. Stehr, C.L. Talcott, N.D. Dutt, N. Venkatasubramanian, A probabilistic formal analysis approach to cross layer optimization in distributed embedded systems, in Bonsangue and Johnsen [59], pp. 285-300.; M. Kim, M.-O. Stehr, C.L. Talcott, N.D. Dutt, N. Venkatasubramanian, A probabilistic formal analysis approach to cross layer optimization in distributed embedded systems, in Bonsangue and Johnsen [59], pp. 285-300.
[262] C. Kirchner, H. Kirchner (Eds.), Proceedings of the Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-À-Mousson, France, September 1-4, 1998, Electronic Notes in Theoretical Computer Science, vol. 15, Elsevier, 1998.; C. Kirchner, H. Kirchner (Eds.), Proceedings of the Second International Workshop on Rewriting Logic and its Applications, WRLA’98, Pont-À-Mousson, France, September 1-4, 1998, Electronic Notes in Theoretical Computer Science, vol. 15, Elsevier, 1998.
[263] C. Kirchner, H. Kirchner, A.S. de Oliveira, Analysis of rewrite-based access control policies, in Dougherty and Escobar [144], pp. 55-75.; C. Kirchner, H. Kirchner, A.S. de Oliveira, Analysis of rewrite-based access control policies, in Dougherty and Escobar [144], pp. 55-75.
[264] H. Kirchner, P.-E. Moreau, Prototyping completion with constraints using computational systems, in Hsiang [243], pp. 438-443.; H. Kirchner, P.-E. Moreau, Prototyping completion with constraints using computational systems, in Hsiang [243], pp. 438-443.
[265] Kirchner, H.; Moreau, P.-E., Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories, Journal of Functional Programming, 11, 2, 207-251 (2001) · Zbl 0979.68055
[266] Kirchner, H.; Ringeissen, C., Combining symbolic constraint solvers on algebraic domains, Journal of Symbolic Computation, 18, 2, 113-155 (1994) · Zbl 0819.68111
[267] H. Kirchner, C. Ringeissen, Constraint solving by narrowing in combined algebraic domains, in: Proceedings of the 11th International Conference on Logic Programming, The MIT Press, 1994, pp. 617-631.; H. Kirchner, C. Ringeissen, Constraint solving by narrowing in combined algebraic domains, in: Proceedings of the 11th International Conference on Logic Programming, The MIT Press, 1994, pp. 617-631.
[268] A. Knapp, Generating rewrite theories from UML collaborations, in Futatsugi et al. [203], pp. 97-120.; A. Knapp, Generating rewrite theories from UML collaborations, in Futatsugi et al. [203], pp. 97-120.
[269] A. Knapp, A Formal Approach to Object-Oriented Software Engineering, Shaker Verlag, Aachen, Germany, 2001, Ph.D. thesis, Institut für Informatik, Universität München, 2000.; A. Knapp, A Formal Approach to Object-Oriented Software Engineering, Shaker Verlag, Aachen, Germany, 2001, Ph.D. thesis, Institut für Informatik, Universität München, 2000.
[270] G. Kniesel, J.S. Pinto (Eds.), Preliminary Proceedings of the Ninth International Workshop on Rule-Based Programming, RULE 2008, Hagenberg Castle, Austria, June 18, 2008, 2008, Technical report IAI-TR-08-02, Institut für Informatik III, Rheinische Friedrich-Wilhelm-Universität Bonn.; G. Kniesel, J.S. Pinto (Eds.), Preliminary Proceedings of the Ninth International Workshop on Rule-Based Programming, RULE 2008, Hagenberg Castle, Austria, June 18, 2008, 2008, Technical report IAI-TR-08-02, Institut für Informatik III, Rheinische Friedrich-Wilhelm-Universität Bonn.
[271] Kolch, W., Meaningful relationships: the regulation of the Ras/Raf/MEK/ERK pathway by protein interactions, Biochemical Journal, 351, 289-305 (2000)
[272] G. Koob, D. Maughan, S. Saydjari (Eds.), Proceedings of the DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25-27, 2000, IEEE Computer Society Press, 2000.; G. Koob, D. Maughan, S. Saydjari (Eds.), Proceedings of the DARPA Information Survivability Conference and Exposition, DISCEX 2000, Hilton Head Island, South Carolina, January 25-27, 2000, IEEE Computer Society Press, 2000.
[273] P. Kosiuczenko, M. Wirsing, Timed rewriting logic for the specification of time-sensitive systems, in: H. Schwichtenberg (Ed.), Proceedings of the NATO Advanced Study Institute on Logic of Computation, Held in Marktoberdorf, Germany, July 25-August 6, 1997, NATO ASI Series F: Computer and Systems Sciences, vol. 157, Springer, 1997, pp. 229-264.; P. Kosiuczenko, M. Wirsing, Timed rewriting logic for the specification of time-sensitive systems, in: H. Schwichtenberg (Ed.), Proceedings of the NATO Advanced Study Institute on Logic of Computation, Held in Marktoberdorf, Germany, July 25-August 6, 1997, NATO ASI Series F: Computer and Systems Sciences, vol. 157, Springer, 1997, pp. 229-264. · Zbl 0876.03015
[274] Kosiuczenko, P.; Wirsing, M., Timed rewriting logic with an application to object-based specification, Science of Computer Programming, 28, 2-3, 225-246 (1997) · Zbl 0877.68071
[275] Koymans, R., Specifying real-time properties with metric temporal logic, Real-Time Systems, 2, 4, 255-299 (1990)
[276] N. Kumar, K. Sen, J. Meseguer, G. Agha, Probabilistic rewrite theories: unifying models, logics and tools, Technical report UIUCDCS-R-2003-2347, Department of Computer Science, University of Illinois at Urbana-Champaign, May 2003.; N. Kumar, K. Sen, J. Meseguer, G. Agha, Probabilistic rewrite theories: unifying models, logics and tools, Technical report UIUCDCS-R-2003-2347, Department of Computer Science, University of Illinois at Urbana-Champaign, May 2003.
[277] N. Kumar, K. Sen, J. Meseguer, G. Agha, A rewriting based model for probabilistic distributed object systems, in Najm et al. [349], pp. 32-46.; N. Kumar, K. Sen, J. Meseguer, G. Agha, A rewriting based model for probabilistic distributed object systems, in Najm et al. [349], pp. 32-46. · Zbl 1253.68244
[278] Laneve, C.; Montanari, U., Axiomatizing permutation equivalence, Mathematical Structures in Computer Science, 6, 3, 219-249 (1996) · Zbl 0884.68070
[279] Lawvere, F. W., Functorial semantics of algebraic theories, Proceedings, National Academy of Sciences, 50, 869-873 (1963), Summary of Ph.D. thesis, Columbia University · Zbl 0119.25901
[280] Lee, E. A., Modeling concurrent real-time processes using discrete events, Annals of Software Engineering, 7, 25-45 (1999)
[281] M. LeMay, C.A. Gunter, Cumulative attestation kernels for embedded systems, in Backes and Ning [36], pp. 655-670.; M. LeMay, C.A. Gunter, Cumulative attestation kernels for embedded systems, in Backes and Ning [36], pp. 655-670.
[282] D. Lepri, E. Ábrahám, P. Ölveczky, Timed CTL model checking in Real-Time Maude, in: Proceedings of the WRLA, Springer LNCS, 2012, submitted for publication.; D. Lepri, E. Ábrahám, P. Ölveczky, Timed CTL model checking in Real-Time Maude, in: Proceedings of the WRLA, Springer LNCS, 2012, submitted for publication. · Zbl 1366.68176
[283] D. Lepri, P.C. Ölveczky, E. Ábrahám, Model checking classes of metric LTL properties of object-oriented Real-Time Maude specifications, in Ölveczky [361], pp. 117-136.; D. Lepri, P.C. Ölveczky, E. Ábrahám, Model checking classes of metric LTL properties of object-oriented Real-Time Maude specifications, in Ölveczky [361], pp. 117-136.
[284] M. Leuschel, A. Podelski (Eds.), Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2007, Wroclaw, Poland, July 14-16, 2007, ACM, 2007.; M. Leuschel, A. Podelski (Eds.), Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2007, Wroclaw, Poland, July 14-16, 2007, ACM, 2007.
[285] E. Lien, Formal Modelling and Analysis of the NORM Multicast Protocol Using Real-Time Maude, Master’s thesis, Department of Linguistics, University of Oslo, April 2004.; E. Lien, Formal Modelling and Analysis of the NORM Multicast Protocol Using Real-Time Maude, Master’s thesis, Department of Linguistics, University of Oslo, April 2004.
[286] E. Lien, P.C. Ölveczky, Formal modeling and analysis of an IETF multicast protocol, in: D.V. Hung, P. Krishnan (Eds.), Proceedings of the Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, November 23-27, 2009, IEEE Computer Society, 2009, pp. 273-282.; E. Lien, P.C. Ölveczky, Formal modeling and analysis of an IETF multicast protocol, in: D.V. Hung, P. Krishnan (Eds.), Proceedings of the Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, November 23-27, 2009, IEEE Computer Society, 2009, pp. 273-282.
[287] L. Liquori, B. Wack, The polymorphic rewriting-calculus: [type checking vs. type inference], in Martı´-Oliet [297], pp. 89-111.; L. Liquori, B. Wack, The polymorphic rewriting-calculus: [type checking vs. type inference], in Martı´-Oliet [297], pp. 89-111. · Zbl 1272.68191
[288] D. Lucanu, Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions, in: A. Middeldorp (Ed.), Proceedings of the Eighth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2008, Castle of Hagenberg, Austria, July 14, 2008, Electronic Notes in Theoretical Computer Science, vol. 237, Elsevier, 2009, pp. 107-125.; D. Lucanu, Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions, in: A. Middeldorp (Ed.), Proceedings of the Eighth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2008, Castle of Hagenberg, Austria, July 14, 2008, Electronic Notes in Theoretical Computer Science, vol. 237, Elsevier, 2009, pp. 107-125. · Zbl 1294.68081
[289] Lucas, S., Context-sensitive computations in functional and functional logic programs, Journal of Functional and Logic Programming, 1998, 1 (1998) · Zbl 0924.68106
[290] Lucas, S., Context-sensitive rewriting strategies, Information and Computation, 178, 1, 294-343 (2002) · Zbl 1012.68095
[291] Lucas, S.; Marché, C.; Meseguer, J., Operational termination of conditional term rewriting systems, Information Processing Letters, 95, 4, 446-453 (2005) · Zbl 1185.68374
[292] S. Lucas, J. Meseguer, Order-sorted dependency pairs, in: S. Antoy, E. Albert (Eds.), Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2008, Valencia, Spain, July 15-17, 2008, ACM, 2008, pp. 108-119.; S. Lucas, J. Meseguer, Order-sorted dependency pairs, in: S. Antoy, E. Albert (Eds.), Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP 2008, Valencia, Spain, July 15-17, 2008, ACM, 2008, pp. 108-119.
[293] Lucas, S.; Meseguer, J., Termination of just/fair computations in term rewriting, Information and Computation, 206, 5, 652-675 (2008) · Zbl 1146.68040
[294] S. Lucas, J. Meseguer, Operational termination of membership equational programs: the order-sorted way, in Roşu [403], pp. 207-225.; S. Lucas, J. Meseguer, Operational termination of membership equational programs: the order-sorted way, in Roşu [403], pp. 207-225. · Zbl 1347.68198
[295] Manolios, P., A compositional theory of refinement for branching time, (CHARME 2003. CHARME 2003, Lecture Notes in Computer Science, vol. 2860 (2003), Springer), 304-318 · Zbl 1179.68088
[296] Marché, C.; Urbain, X., Modular and incremental proofs of AC-termination, Journal of Symbolic Computation, 38, 1, 873-897 (2004) · Zbl 1137.68419
[297] N. Martı´-Oliet (Ed.), Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004, Electronic Notes in Theoretical Computer Science, vol. 117, Elsevier, 2004.; N. Martı´-Oliet (Ed.), Proceedings of the Fifth International Workshop on Rewriting Logic and its Applications, WRLA 2004, Barcelona, Spain, March 27-April 4, 2004, Electronic Notes in Theoretical Computer Science, vol. 117, Elsevier, 2004.
[298] Martı´-Oliet, N.; Meseguer, J., General logics and logical frameworks, (Gabbay, D. M., What is a Logical System?. What is a Logical System?, Studies in Logic and Computation, vol. 4 (1994), Oxford University Press), 355-392 · Zbl 0817.03005
[299] Martı´-Oliet, N.; Meseguer, J., Action and change in rewriting logic, (Pareschi, R.; Fronhöfer, B., Dynamic Worlds: From the Frame Problem to Knowledge Management. Dynamic Worlds: From the Frame Problem to Knowledge Management, Applied Logic Series, vol. 2 (1999), Kluwer Academic Publishers), 1-53 · Zbl 0930.03028
[300] Martı´-Oliet, N.; Meseguer, J., Rewriting logic as a logical and semantic framework, (Gabbay, D. M.; Guenthner, F., Handbook of Philosophical Logic, vol. 9 (2002), Kluwer Academic Publishers.), 1-87
[301] Martı´-Oliet, N.; Meseguer, J., Rewriting logic: roadmap and bibliography, Theoretical Computer Science, 285, 2, 121-154 (2002) · Zbl 1027.68613
[302] N. Martı´-Oliet, J. Meseguer, M. Palomino, Theoroidal maps as algebraic simulations, in: J.L. Fiadeiro, P.D. Mosses, F. Orejas (Eds.), Recent Trends in Algebraic Development Techniques, 17th International Workshop, WADT 2004, Barcelona, Spain, March 27-29, 2004, Revised Selected Papers, Lecture Notes in Computer Science, vol. 3423, Springer, 2004, pp. 126-143.; N. Martı´-Oliet, J. Meseguer, M. Palomino, Theoroidal maps as algebraic simulations, in: J.L. Fiadeiro, P.D. Mosses, F. Orejas (Eds.), Recent Trends in Algebraic Development Techniques, 17th International Workshop, WADT 2004, Barcelona, Spain, March 27-29, 2004, Revised Selected Papers, Lecture Notes in Computer Science, vol. 3423, Springer, 2004, pp. 126-143. · Zbl 1119.68129
[303] N. Martı´-Oliet, J. Meseguer, A. Verdejo, A rewriting semantics for Maude strategies, in Roşu [403], pp. 227-247.; N. Martı´-Oliet, J. Meseguer, A. Verdejo, A rewriting semantics for Maude strategies, in Roşu [403], pp. 227-247. · Zbl 1347.68199
[304] I.A. Mason, C.L. Talcott, Simple network protocol simulation within Maude, in Futatsugi [200], pp. 274-291.; I.A. Mason, C.L. Talcott, Simple network protocol simulation within Maude, in Futatsugi [200], pp. 274-291.
[305] Matthews, S.; Smaill, A.; Basin, D., Experience with \(FS_0\) as a framework theory, (Huet, G.; Plotkin, G., Logical Environments (1993), Cambridge University Press), 61-82
[306] Meadows, C., The NRL protocol analyzer: an overview, Journal of Logic Programming, 26, 2, 113-131 (1996) · Zbl 0871.68052
[307] P. Meredith, M. Hills, G. Roşu, An executable rewriting logic semantics of K-Scheme, in: D. Dube (Ed.), Proceedings of the 2007 Workshop on Scheme and Functional Programming, SCHEME 2007, Freiburg, Germany, September 30, 2007, Laval University, 2007, pp. 91-103.; P. Meredith, M. Hills, G. Roşu, An executable rewriting logic semantics of K-Scheme, in: D. Dube (Ed.), Proceedings of the 2007 Workshop on Scheme and Functional Programming, SCHEME 2007, Freiburg, Germany, September 30, 2007, Laval University, 2007, pp. 91-103.
[308] P. Meredith, M. Hills, G. Roşu, A K definition of Scheme, Technical report UIUCDCS-R-2007-2907, Department of Computer Science, University of Illinois at Urbana-Champaign, 2007.; P. Meredith, M. Hills, G. Roşu, A K definition of Scheme, Technical report UIUCDCS-R-2007-2907, Department of Computer Science, University of Illinois at Urbana-Champaign, 2007.
[309] P. Meredith, M. Katelman, J. Meseguer, G. Roşu, A formal executable semantics of Verilog, in: B. Jobstmann, L. Carloni (Eds.), Proceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010, Grenoble, France, July 26-28, 2010, IEEE Computer Society, 2010, pp. 179-188.; P. Meredith, M. Katelman, J. Meseguer, G. Roşu, A formal executable semantics of Verilog, in: B. Jobstmann, L. Carloni (Eds.), Proceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010, Grenoble, France, July 26-28, 2010, IEEE Computer Society, 2010, pp. 179-188.
[310] J. Meseguer, General logics, in: H.-D. Ebbinghaus et al. (Eds.), Logic Colloquium’87, North-Holland, 1989, pp. 275-329.; J. Meseguer, General logics, in: H.-D. Ebbinghaus et al. (Eds.), Logic Colloquium’87, North-Holland, 1989, pp. 275-329. · Zbl 0691.03001
[311] J. Meseguer, A logical theory of concurrent objects, in: N. Meyrowitz (Ed.), Proceedings of the ECOOP-OOPSLA’90 Conference on Object-Oriented Programming, Ottawa, Canada, October 21-25, 1990, ACM Press, 1990, pp. 101-115.; J. Meseguer, A logical theory of concurrent objects, in: N. Meyrowitz (Ed.), Proceedings of the ECOOP-OOPSLA’90 Conference on Object-Oriented Programming, Ottawa, Canada, October 21-25, 1990, ACM Press, 1990, pp. 101-115.
[312] J. Meseguer, Rewriting as a unified model of concurrency, in: J.C.M. Baeten, J.W. Klop (Eds.), CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, Lecture Notes in Computer Science, vol. 458, Springer, 1990, pp. 384-400.; J. Meseguer, Rewriting as a unified model of concurrency, in: J.C.M. Baeten, J.W. Klop (Eds.), CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, Lecture Notes in Computer Science, vol. 458, Springer, 1990, pp. 384-400.
[313] J. Meseguer, Rewriting as a unified model of concurrency, Technical report SRI-CSL-90-02, SRI International, Computer Science Laboratory, February 1990, Revised June 1990.; J. Meseguer, Rewriting as a unified model of concurrency, Technical report SRI-CSL-90-02, SRI International, Computer Science Laboratory, February 1990, Revised June 1990. · Zbl 0758.68043
[314] J. Meseguer, Conditional rewriting logic: deduction, models and concurrency, in: S. Kaplan, M. Okada (Eds.), Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, Lecture Notes in Computer Science, vol. 516, Springer, 1991, pp. 64-91.; J. Meseguer, Conditional rewriting logic: deduction, models and concurrency, in: S. Kaplan, M. Okada (Eds.), Conditional and Typed Rewriting Systems, 2nd International CTRS Workshop, Montreal, Canada, June 11-14, 1990, Proceedings, Lecture Notes in Computer Science, vol. 516, Springer, 1991, pp. 64-91.
[315] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science, 96, 1, 73-155 (1992) · Zbl 0758.68043
[316] Meseguer, J., A logical theory of concurrent objects and its realization in the Maude language, (Agha, G.; Wegner, P.; Yonezawa, A., Research Directions in Concurrent Object-Oriented Programming (1993), The MIT Press), 314-390
[317] J. Meseguer (Ed.), Proceedings of the First International Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3-6, 1996, Electronic Notes in Theoretical Computer Science, vol. 4, Elsevier, 1996.; J. Meseguer (Ed.), Proceedings of the First International Workshop on Rewriting Logic and its Applications, WRLA’96, Asilomar, California, September 3-6, 1996, Electronic Notes in Theoretical Computer Science, vol. 4, Elsevier, 1996.
[318] J. Meseguer, Rewriting logic as a semantic framework for concurrency: a progress report, in: U. Montanari, V. Sassone (Eds.), CONCUR ’96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings, Lecture Notes in Computer Science, vol. 1119, Springer, 1996, pp. 331-372.; J. Meseguer, Rewriting logic as a semantic framework for concurrency: a progress report, in: U. Montanari, V. Sassone (Eds.), CONCUR ’96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings, Lecture Notes in Computer Science, vol. 1119, Springer, 1996, pp. 331-372.
[319] J. Meseguer, Membership algebra as a logical framework for equational specification, in Parisi-Presicce [378], pp. 18-61.; J. Meseguer, Membership algebra as a logical framework for equational specification, in Parisi-Presicce [378], pp. 18-61. · Zbl 0903.08009
[320] J. Meseguer, Rewriting logic and Maude: a wide-spectrum semantic framework for object-based distributed systems, in: S.F. Smith, C.L. Talcott (Eds.), Formal Methods for Open Object-Based Distributed Systems IV, IFIP TC6/WG6.1 Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000, Stanford, California, USA, September 6-8, 2000, Proceedings, IFIP Conference Proceedings, vol. 177, Kluwer, 2000, pp. 89-117.; J. Meseguer, Rewriting logic and Maude: a wide-spectrum semantic framework for object-based distributed systems, in: S.F. Smith, C.L. Talcott (Eds.), Formal Methods for Open Object-Based Distributed Systems IV, IFIP TC6/WG6.1 Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000, Stanford, California, USA, September 6-8, 2000, Proceedings, IFIP Conference Proceedings, vol. 177, Kluwer, 2000, pp. 89-117. · Zbl 0968.68079
[321] J. Meseguer, Rewriting logic and Maude: concepts and applications, in: L. Bachmair (Ed.), Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1833, Springer, 2000, pp. 1-26.; J. Meseguer, Rewriting logic and Maude: concepts and applications, in: L. Bachmair (Ed.), Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings, Lecture Notes in Computer Science, vol. 1833, Springer, 2000, pp. 1-26. · Zbl 0964.68069
[322] J. Meseguer, Functorial semantics of rewrite theories, in: H.-J. Kreowski, U. Montanari, F. Orejas, G. Rozenberg, G. Taentzer (Eds.), Formal Methods in Software and Systems Modeling, Essays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 3393, Springer, 2005, pp. 220-235.; J. Meseguer, Functorial semantics of rewrite theories, in: H.-J. Kreowski, U. Montanari, F. Orejas, G. Rozenberg, G. Taentzer (Eds.), Formal Methods in Software and Systems Modeling, Essays Dedicated to Hartmut Ehrig on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 3393, Springer, 2005, pp. 220-235.
[323] J. Meseguer, Localized fairness: a rewriting semantics, in Giesl [209], pp. 250-263.; J. Meseguer, Localized fairness: a rewriting semantics, in Giesl [209], pp. 250-263. · Zbl 1078.68660
[324] J. Meseguer, A rewriting logic sampler, in: D.V. Hung, M. Wirsing (Eds.), Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3722, Springer, 2005, pp. 1-28.; J. Meseguer, A rewriting logic sampler, in: D.V. Hung, M. Wirsing (Eds.), Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3722, Springer, 2005, pp. 1-28. · Zbl 1169.03349
[325] J. Meseguer, The temporal logic of rewriting: a gentle introduction, in: P. Degano, R.D. Nicola, J. Meseguer (Eds.), Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 5065, Springer, 2008, pp. 354-382.; J. Meseguer, The temporal logic of rewriting: a gentle introduction, in: P. Degano, R.D. Nicola, J. Meseguer (Eds.), Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 5065, Springer, 2008, pp. 354-382. · Zbl 1143.68459
[326] J. Meseguer, K. Futatsugi, T. Winkler, 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, November 1992, Research Institute of Software Engineering, 1992, pp. 61-106.; J. Meseguer, K. Futatsugi, T. Winkler, 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, November 1992, Research Institute of Software Engineering, 1992, pp. 61-106.
[327] J. Meseguer, N. Martı´-Oliet, From abstract data types to logical frameworks, in: E. Astesiano, G. Reggio, A. Tarlecki (Eds.), Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30-June 3, 1994, Selected Papers, Lecture Notes in Computer Science, vol. 906, Springer, 1995, pp. 48-80.; J. Meseguer, N. Martı´-Oliet, From abstract data types to logical frameworks, in: E. Astesiano, G. Reggio, A. Tarlecki (Eds.), Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30-June 3, 1994, Selected Papers, Lecture Notes in Computer Science, vol. 906, Springer, 1995, pp. 48-80.
[328] J. Meseguer, U. Montanari, Mapping tile logic into rewriting logic, in Parisi-Presicce [378], pp. 62-91.; J. Meseguer, U. Montanari, Mapping tile logic into rewriting logic, in Parisi-Presicce [378], pp. 62-91. · Zbl 0903.08010
[329] J. Meseguer, P.C. Ölveczky, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, in Dong and Zhu [143], pp. 303-320.; J. Meseguer, P.C. Ölveczky, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, in Dong and Zhu [143], pp. 303-320.
[330] J. Meseguer, P.C. Ölveczky, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, 2010.; J. Meseguer, P.C. Ölveczky, Formalization and correctness of the PALS architectural pattern for distributed real-time systems, Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, 2010.
[331] Meseguer, J.; Palomino, M.; Martı´-Oliet, N., Equational abstractions, Theoretical Computer Science, 403, 2-3, 239-264 (2008) · Zbl 1155.68050
[332] Meseguer, J.; Palomino, M.; Martı´-Oliet, N., Algebraic simulations, Journal of Logic and Algebraic Programming, 79, 2, 103-143 (2010) · Zbl 1184.68300
[333] J. Meseguer, G. Roşu, Rewriting logic semantics: from language specifications to formal analysis tools, in: D. Basin, M. Rusinowitch (Eds.), Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3097, Springer, 2004, pp. 1-44.; J. Meseguer, G. Roşu, Rewriting logic semantics: from language specifications to formal analysis tools, in: D. Basin, M. Rusinowitch (Eds.), Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3097, Springer, 2004, pp. 1-44. · Zbl 1126.68464
[334] Meseguer, J.; Roşu, G., The rewriting logic semantics project, Theoretical Computer Science, 373, 3, 213-237 (2007) · Zbl 1111.68068
[335] J. Meseguer, G. Roşu, The rewriting logic semantics project: a progress report, in: O. Owe, M. Steffen, J.A. Telle (Eds.), Fundamentals of Computation Theory - 18th International Symposium, FCT 2011, Oslo, Norway, August 22-25, 2011, Proceedings, Lecture Notes in Computer Science, vol. 6914, Springer, 2011, pp. 1-37.; J. Meseguer, G. Roşu, The rewriting logic semantics project: a progress report, in: O. Owe, M. Steffen, J.A. Telle (Eds.), Fundamentals of Computation Theory - 18th International Symposium, FCT 2011, Oslo, Norway, August 22-25, 2011, Proceedings, Lecture Notes in Computer Science, vol. 6914, Springer, 2011, pp. 1-37. · Zbl 1342.68198
[336] J. Meseguer, R. Sharykin, Specification and analysis of distributed object-based stochastic hybrid systems, in: J.P. Hespanha, A. Tiwari (Eds.), Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, Lecture Notes in Computer Science, vol. 3927, Springer, 2006, pp. 460-475.; J. Meseguer, R. Sharykin, Specification and analysis of distributed object-based stochastic hybrid systems, in: J.P. Hespanha, A. Tiwari (Eds.), Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, March 29-31, 2006, Proceedings, Lecture Notes in Computer Science, vol. 3927, Springer, 2006, pp. 460-475. · Zbl 1178.68350
[337] J. Meseguer, C.L. Talcott, A partial order event model for concurrent objects, in: J.C.M. Baeten, S. Mauw (Eds.), CONCUR’99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1664, Springer, 1999, pp. 415-430.; J. Meseguer, C.L. Talcott, A partial order event model for concurrent objects, in: J.C.M. Baeten, S. Mauw (Eds.), CONCUR’99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1664, Springer, 1999, pp. 415-430. · Zbl 0939.68084
[338] J. Meseguer, C.L. Talcott, Semantic models for distributed object reflection, in: B. Magnusson (Ed.), ECOOP 2002 - Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 10-14, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2374, Springer, 2002, pp. 1-36.; J. Meseguer, C.L. Talcott, Semantic models for distributed object reflection, in: B. Magnusson (Ed.), ECOOP 2002 - Object-Oriented Programming, 16th European Conference, Malaga, Spain, June 10-14, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2374, Springer, 2002, pp. 1-36. · Zbl 1049.68815
[339] J. Meseguer, P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, in Martı´-Oliet [297], pp. 153-182.; J. Meseguer, P. Thati, Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, in Martı´-Oliet [297], pp. 153-182. · Zbl 1272.68194
[340] Meseguer, J.; Thati, P., Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols, Higher-Order and Symbolic Computation, 20, 1-2, 123-160 (2007) · Zbl 1115.68079
[341] S. Miller, D. Cofer, L. Sha, J. Meseguer, A. Al-Nayeem, Implementing logical synchrony in integrated modular avionics, in: Proceedings of the 28th Digital Avionics Systems Conference, IEEE, 2009.; S. Miller, D. Cofer, L. Sha, J. Meseguer, A. Al-Nayeem, Implementing logical synchrony in integrated modular avionics, in: Proceedings of the 28th Digital Avionics Systems Conference, IEEE, 2009.
[342] J. Misra, Computation orchestration: a basis for wide-area computing, in: M. Broy (Ed.), Proceedings of the NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems Marktoberdorf, Germany, 2004, NATO ASI Series, 2004.; J. Misra, Computation orchestration: a basis for wide-area computing, in: M. Broy (Ed.), Proceedings of the NATO Advanced Study Institute, Engineering Theories of Software Intensive Systems Marktoberdorf, Germany, 2004, NATO ASI Series, 2004.
[343] Misra, J.; Cook, W. R., Computation orchestration, Software and System Modeling, 6, 1, 83-110 (2007)
[344] H. Miyoshi, Modelling conditional rewriting logic in structured categories, in Meseguer [317], pp. 20-34.; H. Miyoshi, Modelling conditional rewriting logic in structured categories, in Meseguer [317], pp. 20-34.
[345] Mokhati, F.; Badri, M., Generating Maude specifications from UML use case diagrams, Journal of Object Technology, 8, 2, 136-319 (2009)
[346] F. Mokhati, P. Gagnon, M. Badri, Verifying UML diagrams with model checking: a rewriting logic based approach, in: A. Mathur, W.E. Wong (Eds.), Proceedings of the Seventh International Conference on Quality Software, QSIC 2007, Portland, Oregon, USA, October 11-12, 2007, IEEE Computer Society, 2007, pp. 356-362.; F. Mokhati, P. Gagnon, M. Badri, Verifying UML diagrams with model checking: a rewriting logic based approach, in: A. Mathur, W.E. Wong (Eds.), Proceedings of the Seventh International Conference on Quality Software, QSIC 2007, Portland, Oregon, USA, October 11-12, 2007, IEEE Computer Society, 2007, pp. 356-362.
[347] 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)
[348] Nadathur, G.; Miller, D., An overview of \(\lambda\) Prolog, (Bowen, K.; Kowalski, R., Fifth International Joint Conference and Symposium on Logic Programming (1988), The MIT Press), 810-827
[349] E. Najm, U. Nestmann, P. Stevens (Eds.), Formal Methods for Open Object-Based Distributed Systems, 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, November 19-21, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2884, Springer, 2003.; E. Najm, U. Nestmann, P. Stevens (Eds.), Formal Methods for Open Object-Based Distributed Systems, 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, November 19-21, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2884, Springer, 2003.
[350] Najm, E.; Stefani, J.-B., A formal semantics for the ODP computational model, Computer Networks and ISDN Systems, 27, 8, 1305-1329 (1995)
[351] S. Nakajima, Using algebraic specification techniques in development of object-oriented frameworks, in Wing et al. [471], pp. 1664-1683.; S. Nakajima, Using algebraic specification techniques in development of object-oriented frameworks, in Wing et al. [471], pp. 1664-1683.
[352] S. Nakajima, K. Futatsugi, An object-oriented modeling method for algebraic specifications in CafeOBJ, in: Proceedings of the 19th International Conference on Software Engineering, ICSE’97, Boston, Massachussets, May 17-23, 1997, ACM Press, 1997.; S. Nakajima, K. Futatsugi, An object-oriented modeling method for algebraic specifications in CafeOBJ, in: Proceedings of the 19th International Conference on Software Engineering, ICSE’97, Boston, Massachussets, May 17-23, 1997, ACM Press, 1997.
[353] P. Naumov, M.-O. Stehr, J. Meseguer, The HOL/NuPRL proof translator (a practical approach to formal interoperability), in: R.J. Boulton, P.B. Jackson (Eds.), Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, Lecture Notes in Computer Science, vol. 2152, Springer, 2001, pp. 329-345.; P. Naumov, M.-O. Stehr, J. Meseguer, The HOL/NuPRL proof translator (a practical approach to formal interoperability), in: R.J. Boulton, P.B. Jackson (Eds.), Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, Lecture Notes in Computer Science, vol. 2152, Springer, 2001, pp. 329-345. · Zbl 1005.68542
[354] Nguyen, Q. H.; Kirchner, C.; Kirchner, H., External rewriting for skeptical proof assistants, Journal of Automated Reasoning, 29, 3-4, 309-336 (2002) · Zbl 1064.68048
[355] R. Nieuwenhuis (Ed.), Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2706, Springer, 2003.; R. Nieuwenhuis (Ed.), Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2706, Springer, 2003.
[356] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T), Journal of the ACM, 53, 6, 937-977 (2006) · Zbl 1326.68164
[357] K. Ogata, K. Futatsugi, Proof scores in the OTS/CafeOBJ method, in Najm et al. [349], pp. 170-184.; K. Ogata, K. Futatsugi, Proof scores in the OTS/CafeOBJ method, in Najm et al. [349], pp. 170-184. · Zbl 1253.68249
[358] Ohlebusch, E., Advanced Topics in Term Rewriting (2002), Springer Verlag · Zbl 0999.68095
[359] P.C. Ölveczky, Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic, Ph.D. thesis, University of Bergen, Norway, 2000.; P.C. Ölveczky, Specification and Analysis of Real-Time and Hybrid Systems in Rewriting Logic, Ph.D. thesis, University of Bergen, Norway, 2000.
[360] P.C. Ölveczky, Towards formal modeling and analysis of networks of embedded medical devices in Real-Time Maude, in: P. Muenchaisri (Ed.), Proceedings of the Ninth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, SNPD 2008, Phuket, Thailand, August 6-8, 2008, IEEE Computer Society, 2008, pp. 241-248.; P.C. Ölveczky, Towards formal modeling and analysis of networks of embedded medical devices in Real-Time Maude, in: P. Muenchaisri (Ed.), Proceedings of the Ninth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing, SNPD 2008, Phuket, Thailand, August 6-8, 2008, IEEE Computer Society, 2008, pp. 241-248.
[361] P.C. Ölveczky (Ed.), Proceedings of the First International Workshop on Rewriting Techniques for Real-Time Systems, RTRTS 2010, Longyearbyen, Spitsbergen, Norway, April 6-9, 2010, Electronic Proceedings in Theoretical Computer Science, vol. 36, Computing Research Repository (CoRR), 2010.; P.C. Ölveczky (Ed.), Proceedings of the First International Workshop on Rewriting Techniques for Real-Time Systems, RTRTS 2010, Longyearbyen, Spitsbergen, Norway, April 6-9, 2010, Electronic Proceedings in Theoretical Computer Science, vol. 36, Computing Research Repository (CoRR), 2010.
[362] P.C. Ölveczky (Ed.), Rewriting Logic and its Applications. 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6381, Springer, 2010.; P.C. Ölveczky (Ed.), Rewriting Logic and its Applications. 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6381, Springer, 2010. · Zbl 1197.68017
[363] P.C. Ölveczky, A. Boronat, J. Meseguer, Formal semantics and analysis of behavioral AADL models in Real-Time Maude, in: J. Hatcliff, E. Zucca (Eds.), Formal Techniques for Distributed Systems, Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010 and 30th IFIP WG 6.1 International Conference, FORTE 2010, Amsterdam, The Netherlands, June 7-9, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6117, Springer, 2010, pp. 47-62.; P.C. Ölveczky, A. Boronat, J. Meseguer, Formal semantics and analysis of behavioral AADL models in Real-Time Maude, in: J. Hatcliff, E. Zucca (Eds.), Formal Techniques for Distributed Systems, Joint 12th IFIP WG 6.1 International Conference, FMOODS 2010 and 30th IFIP WG 6.1 International Conference, FORTE 2010, Amsterdam, The Netherlands, June 7-9, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6117, Springer, 2010, pp. 47-62.
[364] P.C. Ölveczky, M. Caccamo, Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude, in: L. Baresi, R. Heckel (Eds.), Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings, Lecture Notes in Computer Science, vol. 3922, Springer, 2006, pp. 357-372.; P.C. Ölveczky, M. Caccamo, Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude, in: L. Baresi, R. Heckel (Eds.), Fundamental Approaches to Software Engineering, 9th International Conference, FASE 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings, Lecture Notes in Computer Science, vol. 3922, Springer, 2006, pp. 357-372.
[365] P.C. Ölveczky, M. Keaton, J. Meseguer, C.L. Talcott, S. Zabele, Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude, in: H. Hußmann (Ed.), Fundamental Approaches to Software Engineering, 4th International Conference, FASE 2001, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, 2001, Proceedings, Lecture Notes in Computer Science, vol. 2029, Springer, 2001, pp. 333-348.; P.C. Ölveczky, M. Keaton, J. Meseguer, C.L. Talcott, S. Zabele, Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude, in: H. Hußmann (Ed.), Fundamental Approaches to Software Engineering, 4th International Conference, FASE 2001, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Genova, Italy, April 2-6, 2001, Proceedings, Lecture Notes in Computer Science, vol. 2029, Springer, 2001, pp. 333-348. · Zbl 0977.68865
[366] Ölveczky, P. C.; Kosiuczenko, P.; Wirsing, M., An object-oriented algebraic steam-boiler control specification, (Abrial, J.-R.; Börger, E.; Langmaack, H., Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control. Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control, Lecture Notes in Computer Science, vol. 1165 (1996), Springer), 379-402
[367] P.C. Ölveczky, J. Meseguer, Specifying real-time systems in rewriting logic, in Meseguer [317], pp. 284-309.; P.C. Ölveczky, J. Meseguer, Specifying real-time systems in rewriting logic, in Meseguer [317], pp. 284-309. · Zbl 0912.68098
[368] Ö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
[369] P.C. Ölveczky, J. Meseguer, Real-Time Maude 2.1, in Martı´-Oliet [297], pp. 285-314.; P.C. Ölveczky, J. Meseguer, Real-Time Maude 2.1, in Martı´-Oliet [297], pp. 285-314.
[370] P.C. Ölveczky, J. Meseguer, Abstraction and completeness for Real-Time Maude, in Denker and Talcott [139], pp. 5-27.; P.C. Ölveczky, J. Meseguer, Abstraction and completeness for Real-Time Maude, in Denker and Talcott [139], pp. 5-27. · Zbl 1279.68218
[371] Ö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
[372] P.C. Ölveczky, J. Meseguer, Specification and verification of distributed embedded systems: a traffic intersection product family, in Ölveczky [361], pp. 137-157.; P.C. Ölveczky, J. Meseguer, Specification and verification of distributed embedded systems: a traffic intersection product family, in Ölveczky [361], pp. 137-157.
[373] Ölveczky, P. C.; Meseguer, J.; Talcott, C. L., Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude, Formal Methods in System Design, 29, 3, 253-293 (2006) · Zbl 1109.68010
[374] P.C. Ölveczky, P. Prabhakar, X. Liu, Formal modeling and analysis of real-time resource-sharing protocols in Real-Time Maude, in: Y. Robert (Ed.), 22nd IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2008, Miami, Florida USA, April 14-18, 2008, IEEE, 2008, pp. 1-8.; P.C. Ölveczky, P. Prabhakar, X. Liu, Formal modeling and analysis of real-time resource-sharing protocols in Real-Time Maude, in: Y. Robert (Ed.), 22nd IEEE International Symposium on Parallel and Distributed Processing, IPDPS 2008, Miami, Florida USA, April 14-18, 2008, IEEE, 2008, pp. 1-8.
[375] P.C. Ölveczky, S. Thorvaldsen, Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude, in Bonsangue and Johnsen [59], pp. 122-140.; P.C. Ölveczky, S. Thorvaldsen, Formal modeling and analysis of the OGDC wireless sensor network algorithm in Real-Time Maude, in Bonsangue and Johnsen [59], pp. 122-140. · Zbl 1178.68699
[376] Ölveczky, P. C.; Thorvaldsen, S., Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude, Theoretical Computer Science, 410, 2-3, 254-280 (2009) · Zbl 1178.68699
[377] M. Palomino, J. Meseguer, N. Martı´-Oliet, A categorical approach to simulations, in: J.L. Fiadeiro, N. Harman, M. Roggenbach, J.J.M.M. Rutten (Eds.), Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3629, Springer, 2005, pp. 313-330.; M. Palomino, J. Meseguer, N. Martı´-Oliet, A categorical approach to simulations, in: J.L. Fiadeiro, N. Harman, M. Roggenbach, J.J.M.M. Rutten (Eds.), Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3629, Springer, 2005, pp. 313-330. · Zbl 1151.68550
[378] F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3-7, 1997, Selected Papers, Lecture Notes in Computer Science, vol. 1376, Springer, 1997.; F. Parisi-Presicce (Ed.), Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT’97, Tarquinia, Italy, June 3-7, 1997, Selected Papers, Lecture Notes in Computer Science, vol. 1376, Springer, 1997. · Zbl 0889.00030
[379] K. Pattabiraman, N. Nakka, Z. Kalbarczyk, R.K. Iyer, SymPLFIED: symbolic program-level fault injection and error detection framework, in: Proceedings of the 38th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2008, Anchorage, Alaska, USA, June 24-27, 2008, IEEE Computer Society, 2008, pp. 472-481.; K. Pattabiraman, N. Nakka, Z. Kalbarczyk, R.K. Iyer, SymPLFIED: symbolic program-level fault injection and error detection framework, in: Proceedings of the 38th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2008, Anchorage, Alaska, USA, June 24-27, 2008, IEEE Computer Society, 2008, pp. 472-481. · Zbl 1365.68090
[380] K. Pattabiraman, N. Nakka, Z. Kalbarczyk, R.K. Iyer, Discovering application-level insider attacks using symbolic execution, in: D. Gritzalis, J. Lopez (Eds.), Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18-20, 2009, Proceedings, IFIP Advances in Information and Communication Technology, vol. 297, Springer, 2009, pp. 63-75.; K. Pattabiraman, N. Nakka, Z. Kalbarczyk, R.K. Iyer, Discovering application-level insider attacks using symbolic execution, in: D. Gritzalis, J. Lopez (Eds.), Emerging Challenges for Security, Privacy and Trust, 24th IFIP TC 11 International Information Security Conference, SEC 2009, Pafos, Cyprus, May 18-20, 2009, Proceedings, IFIP Advances in Information and Communication Technology, vol. 297, Springer, 2009, pp. 63-75.
[381] Paulson, L. C., Isabelle, Lecture Notes in Computer Science, vol. 828 (1994), Springer Verlag · Zbl 0825.68059
[382] (Paun, G., Membrane Computing. An Introduction (2002), Springer) · Zbl 1034.68037
[383] Peterson, G. E.; Stickel, M. E., Complete sets of reductions for some equational theories, Journal of the Association for Computing Machinery, 28, 2, 233-264 (1981) · Zbl 0479.68092
[384] F. Pfenning, Elf: a language for logic definition and verified metaprogramming, in: Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, Asilomar, California, June 1989, pp. 313-322.; F. Pfenning, Elf: a language for logic definition and verified metaprogramming, in: Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, Asilomar, California, June 1989, pp. 313-322. · Zbl 0716.68079
[385] A. Pnueli, Deduction is forever, invited talk at FM’99, 1999. Avaliable from: <http://cs.nyu.edu/pnueli/fm99.ps>; A. Pnueli, Deduction is forever, invited talk at FM’99, 1999. Avaliable from: <http://cs.nyu.edu/pnueli/fm99.ps>
[386] Porat, S.; Francez, N., Fairness in term rewriting systems, (RTA’85. RTA’85, LNCS, vol. 202 (1985), Springer), 287-300 · Zbl 0576.68040
[387] Porat, S.; Francez, N., Full-commutation and fair-termination in equational (and combined) term-rewriting systems, (CADE’86. CADE’86, LNCS, vol. 230 (1986), Springer), 21-41 · Zbl 0642.68039
[388] Puterman, M., Markov Decision Processes: Discrete Stochastic Dynamic Programming (1994), John Wiley and Sons · Zbl 0829.90134
[389] C. Rattray, S. Maharaj, C. Shankland (Eds.), Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3116, Springer, 2004.; C. Rattray, S. Maharaj, C. Shankland (Eds.), Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3116, Springer, 2004.
[390] S. Reich, Implementing and Extending the MSR Crypto-Protocol Specification Language, Master’s thesis, Fachbereich Informatik, Universität Hamburg, April 2006.; S. Reich, Implementing and Extending the MSR Crypto-Protocol Specification Language, Master’s thesis, Fachbereich Informatik, Universität Hamburg, April 2006.
[391] A. Riesco, A. Verdejo, Implementing and analyzing in Maude the Enhanced Interior Gateway Routing Protocol, in Roşu [403], pp. 249-266.; A. Riesco, A. Verdejo, Implementing and analyzing in Maude the Enhanced Interior Gateway Routing Protocol, in Roşu [403], pp. 249-266.
[392] A. Riesco, A. Verdejo, N. Martı´-Oliet, R. Caballero, Declarative debugging of rewriting logic specifications, Journal of Logic and Algebraic Programming, this volume.; A. Riesco, A. Verdejo, N. Martı´-Oliet, R. Caballero, Declarative debugging of rewriting logic specifications, Journal of Logic and Algebraic Programming, this volume. · Zbl 1253.68097
[393] J.E. Rivera, F. Durán, A. Vallecillo, A graphical approach for modeling time-dependent behavior of DSLs, in: R. DeLine, M. Minas (Eds.), Proceedings of the IEEE Symposium on Visual Languages and Human-Centric Computing, VL/HCC 2009, Corvallis, OR, USA, September 20-24, 2009, IEEE, 2009, pp. 51-55.; J.E. Rivera, F. Durán, A. Vallecillo, A graphical approach for modeling time-dependent behavior of DSLs, in: R. DeLine, M. Minas (Eds.), Proceedings of the IEEE Symposium on Visual Languages and Human-Centric Computing, VL/HCC 2009, Corvallis, OR, USA, September 20-24, 2009, IEEE, 2009, pp. 51-55.
[394] J.E. Rivera, F. Durán, A. Vallecillo, On the behavioral semantics of real-time domain specific visual languages, in Ölveczky [362], pp. 174-190.; J.E. Rivera, F. Durán, A. Vallecillo, On the behavioral semantics of real-time domain specific visual languages, in Ölveczky [362], pp. 174-190.
[395] Rocha, C.; Meseguer, J., A rewriting decision procedure for Dijkstra-Scholten’s syllogistic logic with complements, Revista Colombiana de Computación, 8, 2 (2007)
[396] C. Rocha, J. Meseguer, Theorem proving modulo based on Boolean equational procedures, in: R. Berghammer, B. Möller, G. Struth (Eds.), Relations and Kleene Algebra in Computer Science, 10th International Conference on Relational Methods in Computer Science, and 5th International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008, Frauenwörth, Germany, April 7-11, 2008, Proceedings, Lecture Notes in Computer Science, vol. 4988, Springer, 2008, pp. 337-351.; C. Rocha, J. Meseguer, Theorem proving modulo based on Boolean equational procedures, in: R. Berghammer, B. Möller, G. Struth (Eds.), Relations and Kleene Algebra in Computer Science, 10th International Conference on Relational Methods in Computer Science, and 5th International Conference on Applications of Kleene Algebra, RelMiCS/AKA 2008, Frauenwörth, Germany, April 7-11, 2008, Proceedings, Lecture Notes in Computer Science, vol. 4988, Springer, 2008, pp. 337-351. · Zbl 1139.03010
[397] C. Rocha, J. Meseguer, Constructors, sufficient completeness and deadlock freedom of rewrite theories, in: C.G. Fermüller, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6397, Springer, 2010, pp. 594-609.; C. Rocha, J. Meseguer, Constructors, sufficient completeness and deadlock freedom of rewrite theories, in: C.G. Fermüller, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6397, Springer, 2010, pp. 594-609. · Zbl 1306.68087
[398] C. Rocha, J. Meseguer, Proving safety properties of rewrite theories, in Corradini et al. [124], pp. 314-328.; C. Rocha, J. Meseguer, Proving safety properties of rewrite theories, in Corradini et al. [124], pp. 314-328. · Zbl 1344.68142
[399] C. Rocha, C. Muñoz, H. Cadavid, A graphical environment for the semantic validation of a plan execution language, in: S. Grenander, L. Bergman (Eds.), Proceedings of the Third IEEE International Conference on Space Mission Challenges for Information Technology, SMC-IT 2009, Pasadena, California, USA, July 19-23, 2009, IEEE Computer Society, Los Alamitos, CA, USA, 2009, pp. 201-207.; C. Rocha, C. Muñoz, H. Cadavid, A graphical environment for the semantic validation of a plan execution language, in: S. Grenander, L. Bergman (Eds.), Proceedings of the Third IEEE International Conference on Space Mission Challenges for Information Technology, SMC-IT 2009, Pasadena, California, USA, July 19-23, 2009, IEEE Computer Society, Los Alamitos, CA, USA, 2009, pp. 201-207.
[400] D.E. Rodrı´guez, Case studies in the specification and analysis of protocols in Maude, in Futatsugi [200], pp. 257-273.; D.E. Rodrı´guez, Case studies in the specification and analysis of protocols in Maude, in Futatsugi [200], pp. 257-273.
[401] D.E. Rodrı´guez, A secret-sharing protocol modelled in Maude, in Gadducci and Montanari [205], pp. 223-239.; D.E. Rodrı´guez, A secret-sharing protocol modelled in Maude, in Gadducci and Montanari [205], pp. 223-239. · Zbl 1272.94088
[402] Romero, J. R.; Vallecillo, A.; Durán, F., Writing and executing ODP computational viewpoint specifications using Maude, Computer Standards & Interfaces, 29, 4, 481-498 (2007)
[403] G. Roşu (Ed.), Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008, Electronic Notes in Theoretical Computer Science, vol. 238(3), Elsevier, 2009.; G. Roşu (Ed.), Proceedings of the Seventh International Workshop on Rewriting Logic and its Applications, WRLA 2008, Budapest, Hungary, March 29-30, 2008, Electronic Notes in Theoretical Computer Science, vol. 238(3), Elsevier, 2009.
[404] G. Roşu, A. Ştefănescu, Matching logic: a new program verification approach (new ideas and emerging results track), in: R.N. Taylor, H. Gall, N. Medvidovic (Eds.), Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011, ACM, 2011, pp. 868-871.; G. Roşu, A. Ştefănescu, Matching logic: a new program verification approach (new ideas and emerging results track), in: R.N. Taylor, H. Gall, N. Medvidovic (Eds.), Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu , HI, USA, May 21-28, 2011, ACM, 2011, pp. 868-871.
[405] G. Roşu, S. Eker, P. Lincoln, J. Meseguer, Certifying and synthesizing membership equational proofs, in: K. Araki, S. Gnesi, D. Mandrioli (Eds.), FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2805, Springer, 2003, pp. 359-380.; G. Roşu, S. Eker, P. Lincoln, J. Meseguer, Certifying and synthesizing membership equational proofs, in: K. Araki, S. Gnesi, D. Mandrioli (Eds.), FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2805, Springer, 2003, pp. 359-380.
[406] G. Roşu, C. Ellison, W. Schulte, Matching logic: an alternative to Hoare/Floyd logic, in Johnson and Pavlovic [246], pp. 142-162.; G. Roşu, C. Ellison, W. Schulte, Matching logic: an alternative to Hoare/Floyd logic, in Johnson and Pavlovic [246], pp. 142-162. · Zbl 1308.68045
[407] G. Roşu, W. Schulte, T.F. Şerbănuţă, Runtime verification of C memory safety, in: S. Bensalem, D. Peled (Eds.), Runtime Verification, 9th International Workshop, RV 2009, Grenoble, France, June 26-28, 2009, Selected Papers, Lecture Notes in Computer Science, vol. 5779, Springer, 2009, pp. 132-151.; G. Roşu, W. Schulte, T.F. Şerbănuţă, Runtime verification of C memory safety, in: S. Bensalem, D. Peled (Eds.), Runtime Verification, 9th International Workshop, RV 2009, Grenoble, France, June 26-28, 2009, Selected Papers, Lecture Notes in Computer Science, vol. 5779, Springer, 2009, pp. 132-151.
[408] Roşu, G.; Şerb&abreve;nuţ&abreve;, T. F., An overview of the K semantic framework, Journal of Logic and Algebraic Programming, 79, 6, 397-434 (2010)
[409] V. Rusu, Combining theorem proving and narrowing for rewriting-logic specifications, in: G. Fraser, A. Gargantini (Eds.), Tests and Proofs, 4th International Conference, TAP 2010, Málaga, Spain, July 1-2, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6143, Springer, 2010, pp. 135-150.; V. Rusu, Combining theorem proving and narrowing for rewriting-logic specifications, in: G. Fraser, A. Gargantini (Eds.), Tests and Proofs, 4th International Conference, TAP 2010, Málaga, Spain, July 1-2, 2010, Proceedings, Lecture Notes in Computer Science, vol. 6143, Springer, 2010, pp. 135-150.
[410] V. Rusu, M. Clavel, Vérification d’invariants pour des systèmes spécifiés en logique de réÉcriture, in: A. Schmitt (Ed.), JFLA 2009, Vingtièmes Journées Francophones des Langages Applicatifs, Saint Quentin sur Isère, France, January 31-February 3, 2009, Proceedings, Studia Informatica Universalis, vol. 7.2, 2009, pp. 317-350.; V. Rusu, M. Clavel, Vérification d’invariants pour des systèmes spécifiés en logique de réÉcriture, in: A. Schmitt (Ed.), JFLA 2009, Vingtièmes Journées Francophones des Langages Applicatifs, Saint Quentin sur Isère, France, January 31-February 3, 2009, Proceedings, Studia Informatica Universalis, vol. 7.2, 2009, pp. 317-350.
[411] G. Santos-Garcı´a, M. Palomino, A. Verdejo, Rewriting logic using strategies for neural networks: an implementation in Maude, in: J.M. Corchado, S. Rodrı´guez, J. Llinas, J.M. Molina (Eds.), Proceedings of the International Symposium on Distributed Computing and Artificial Intelligence, DCAI 2008, University of Salamanca, Spain, October 22-24, 2008, Advances in Soft Computing, vol. 50, Springer, 2009, pp. 424-433.; G. Santos-Garcı´a, M. Palomino, A. Verdejo, Rewriting logic using strategies for neural networks: an implementation in Maude, in: J.M. Corchado, S. Rodrı´guez, J. Llinas, J.M. Molina (Eds.), Proceedings of the International Symposium on Distributed Computing and Artificial Intelligence, DCAI 2008, University of Salamanca, Spain, October 22-24, 2008, Advances in Soft Computing, vol. 50, Springer, 2009, pp. 424-433.
[412] R. Sasse, S. Escobar, C. Meadows, J. Meseguer, Protocol analysis modulo combination of theories: a case study in Maude-NPA, in: J. Cuéllar, J. Lopez, G. Barthe, A. Pretschner (Eds.), Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6710, Springer, 2011, pp. 163-178.; R. Sasse, S. Escobar, C. Meadows, J. Meseguer, Protocol analysis modulo combination of theories: a case study in Maude-NPA, in: J. Cuéllar, J. Lopez, G. Barthe, A. Pretschner (Eds.), Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6710, Springer, 2011, pp. 163-178.
[413] R. Sasse, J. Meseguer, Java+ITP: a verification tool based on Hoare logic and algebraic semantics, in Denker and Talcott [139], pp. 29-46.; R. Sasse, J. Meseguer, Java+ITP: a verification tool based on Hoare logic and algebraic semantics, in Denker and Talcott [139], pp. 29-46.
[414] Schernhammer, F.; Gramlich, B., Characterizing and proving operational termination of deterministic conditional term rewriting systems, Journal of Logic and Algebraic Programming, 79, 7, 659-688 (2010) · Zbl 1206.68163
[415] F. Schernhammer, J. Meseguer, Incremental checking of well-founded recursive specifications modulo axioms, in Schneider-Kamp and Hanus [416], pp. 5-16.; F. Schernhammer, J. Meseguer, Incremental checking of well-founded recursive specifications modulo axioms, in Schneider-Kamp and Hanus [416], pp. 5-16.
[416] P. Schneider-Kamp, M. Hanus (Eds.), Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming, PPDP 2011, Odense, Denmark, July 20-22, 2011, ACM, 2011.; P. Schneider-Kamp, M. Hanus (Eds.), Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming, PPDP 2011, Odense, Denmark, July 20-22, 2011, ACM, 2011.
[417] C. Schürmann, M.-O. Stehr, An executable formalization of the HOL/Nuprl connection in the metalogical framework Twelf, in: M. Hermann, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4246, Springer, 2006, pp. 150-166.; C. Schürmann, M.-O. Stehr, An executable formalization of the HOL/Nuprl connection in the metalogical framework Twelf, in: M. Hermann, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4246, Springer, 2006, pp. 150-166. · Zbl 1165.68473
[418] R. Segala, Modelling and Verification of Randomized Distributed Real Time Systems, Ph.D. thesis, Massachusetts Institute of Technology, 1995.; R. Segala, Modelling and Verification of Randomized Distributed Real Time Systems, Ph.D. thesis, Massachusetts Institute of Technology, 1995.
[419] Sen, K.; Viswanathan, M.; Agha, G., On statistical model checking of stochastic systems, (17th conference on Computer Aided Verification (CAV’05). 17th conference on Computer Aided Verification (CAV’05), LNCS, vol. 3576 (2005), Springer: Springer Edinburgh, Scotland), 266-280 · Zbl 1081.68635
[420] K. Sen, M. Viswanathan, G.A. Agha, VESTA: a statistical model-checker and analyzer for probabilistic systems, in: QEST 2005, 2005, pp. 251-252.; K. Sen, M. Viswanathan, G.A. Agha, VESTA: a statistical model-checker and analyzer for probabilistic systems, in: QEST 2005, 2005, pp. 251-252.
[421] T.F. Şerbănuţă, A Rewriting Approach to Concurrent Programming Language Design and Semantics, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, 2010. Available from: <http://hdl.handle.net/2142/18252>; T.F. Şerbănuţă, A Rewriting Approach to Concurrent Programming Language Design and Semantics, Ph.D. thesis, Department of Computer Science, University of Illinois at Urbana-Champaign, 2010. Available from: <http://hdl.handle.net/2142/18252>
[422] T.F. Şerbănuţă, G. Roşu, K-Maude: a rewriting based tool for semantics of programming languages, in Ölveczky [362], pp. 104-122.; T.F. Şerbănuţă, G. Roşu, K-Maude: a rewriting based tool for semantics of programming languages, in Ölveczky [362], pp. 104-122.
[423] Şerb&abreve;nuţ&abreve;, T. F.; Roşu, G.; Meseguer, J., A rewriting logic approach to operational semantics, Information and Computation, 207, 2, 305-340 (2009)
[424] R. Shankesi, M. AlTurki, R. Sasse, C.A. Gunter, J. Meseguer, Model-checking DoS amplification for VoIP session initiation, in Backes and Ning [36], pp. 390-405.; R. Shankesi, M. AlTurki, R. Sasse, C.A. Gunter, J. Meseguer, Model-checking DoS amplification for VoIP session initiation, in Backes and Ning [36], pp. 390-405.
[425] Smullyan, R. M., Theory of Formal Systems, Annals of Mathematics Studies, vol. 47 (1961), Princeton University Press · Zbl 0218.02030
[426] Sriram, M. G., Modelling protein functional domains in signal transduction using Maude, Briefings in Bioinformatics, 4, 3, 236-245 (2003)
[427] J.R. Stanton, Y. Amir, D. Hasse, G. Ateniese, Y. Kim, C. Nita-Rotaru, T. Schlossnagle, J.L. Schultz, G. Tsudik, Secure group communication in asynchronous networks with failures: Integration and experiments, in: ICDCS, 2000, pp. 330-343.; J.R. Stanton, Y. Amir, D. Hasse, G. Ateniese, Y. Kim, C. Nita-Rotaru, T. Schlossnagle, J.L. Schultz, G. Tsudik, Secure group communication in asynchronous networks with failures: Integration and experiments, in: ICDCS, 2000, pp. 330-343.
[428] V. Stavridou, J.A. Goguen, A. Stevens, S.M. Eker, S.N. Aloneftis, K.M. Hobley, Funnel and 2obj: towards an integrated hardware design environment, in: Theorem Provers in Circuit Design (TPDC), Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, IFIP Transactions, vol. A-10, North-Holland, 1992, pp. 197-223.; V. Stavridou, J.A. Goguen, A. Stevens, S.M. Eker, S.N. Aloneftis, K.M. Hobley, Funnel and 2obj: towards an integrated hardware design environment, in: Theorem Provers in Circuit Design (TPDC), Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, IFIP Transactions, vol. A-10, North-Holland, 1992, pp. 197-223.
[429] L.J. Steggles, P. Kosiuczenko, A timed rewriting logic semantics for SDL: a case study of the alternating bit protocol, in Kirchner and Kirchner [262], pp. 83-104.; L.J. Steggles, P. Kosiuczenko, A timed rewriting logic semantics for SDL: a case study of the alternating bit protocol, in Kirchner and Kirchner [262], pp. 83-104. · Zbl 0917.68116
[430] M.-O. Stehr, CINNI — a generic calculus of explicit substitutions and its application to \(\operatorname{\Lambda;} \operatorname{\Sigmav;} \operatorname{\Pi;} \); M.-O. Stehr, CINNI — a generic calculus of explicit substitutions and its application to \(\operatorname{\Lambda;} \operatorname{\Sigmav;} \operatorname{\Pi;} \)
[431] M.-O. Stehr, Programming, Specification, and Interactive Theorem Proving — Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory, Ph.D. thesis, Fachbereich Informatik, Universität Hamburg, 2002.; M.-O. Stehr, Programming, Specification, and Interactive Theorem Proving — Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory, Ph.D. thesis, Fachbereich Informatik, Universität Hamburg, 2002.
[432] Stehr, M.-O., The open calculus of constructions (part I): an equational type theory with dependent types for programming, specification, and interactive theorem proving, Fundamenta Informaticae, 68, 1-2, 131-174 (2005) · Zbl 1103.03032
[433] Stehr, M.-O., The open calculus of constructions (part II): an equational type theory with dependent types for programming, specification, and interactive theorem proving, Fundamenta Informaticae, 68, 3, 249-288 (2005) · Zbl 1103.03033
[434] Stehr, M.-O.; Meseguer, J., Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework, (Owe, O.; Krogdahl, S.; Lyche, T., From Object-Orientation to Formal Methods, Essays in Memory of Ole-Johan Dahl. From Object-Orientation to Formal Methods, Essays in Memory of Ole-Johan Dahl, Lecture Notes in Computer Science, vol. 2635 (2004), Springer), 334-375 · Zbl 1278.03066
[435] Stehr, M.-O.; Meseguer, J.; Ölveczky, P. C., Rewriting logic as a unifying framework for Petri nets, (Ehrig, H.; Juhás, G.; Padberg, J.; Rozenberg, G., Unifying Petri Nets, Advances in Petri Nets. Unifying Petri Nets, Advances in Petri Nets, Lecture Notes in Computer Science, vol. 2128 (2001), Springer), 250-303 · Zbl 1017.68080
[436] J.G. Stell, Modelling term rewriting systems by sesqui-categories, Technical report TR94-02, Keele University, 1994.; J.G. Stell, Modelling term rewriting systems by sesqui-categories, Technical report TR94-02, Keele University, 1994.
[437] Stewart, W. J., Introduction to the Numerical Solution of Markov Chains (1994), Princeton · Zbl 0821.65099
[438] M. Sun, J. Meseguer, Distributed real-time emulation of formally-defined patterns for safe medical device control, in Ölveczky [361], pp. 158-177.; M. Sun, J. Meseguer, Distributed real-time emulation of formally-defined patterns for safe medical device control, in Ölveczky [361], pp. 158-177.
[439] M. Sun, J. Meseguer, L. Sha, A formal pattern architecture for safe medical systems, in Ölveczky [362], pp. 157-173.; M. Sun, J. Meseguer, L. Sha, A formal pattern architecture for safe medical systems, in Ölveczky [362], pp. 157-173. · Zbl 1306.68090
[440] Talcott, C. L., Actor theories in rewriting logic, Theoretical Computer Science, 285, 2, 441-485 (2002) · Zbl 1001.68055
[441] C.L. Talcott, Coordination models based on a formal model of distributed object reflection, in: L. Brim, I. Linden (Eds.), Proceedings of the First International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord 2005, Namur, Belgium, April 23, 2005, Electronic Notes in Theoretical Computer Science, vol. 150(1), Elsevier, 2006, pp. 143-157.; C.L. Talcott, Coordination models based on a formal model of distributed object reflection, in: L. Brim, I. Linden (Eds.), Proceedings of the First International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord 2005, Namur, Belgium, April 23, 2005, Electronic Notes in Theoretical Computer Science, vol. 150(1), Elsevier, 2006, pp. 143-157.
[442] C.L. Talcott, Formal executable models of cell signaling primitives, in: T. Margaria, B. Steffen (Eds.), Proceedings of the Leveraging Applications of Formal Methods Second International Symposium, ISoLA 2006, Paphos, Cyprus, November 15-19, 2006, IEEE, 2006, pp. 298-302.; C.L. Talcott, Formal executable models of cell signaling primitives, in: T. Margaria, B. Steffen (Eds.), Proceedings of the Leveraging Applications of Formal Methods Second International Symposium, ISoLA 2006, Paphos, Cyprus, November 15-19, 2006, IEEE, 2006, pp. 298-302.
[443] C.L. Talcott, Symbolic modeling of signal transduction in Pathway Logic, in: L.F. Perrone, B. Lawson, J. Liu, F.P. Wieland (Eds.), Proceedings of the Winter Simulation Conference, WSC 2006, Monterey, California, USA, December 3-6, 2006, WSC, 2006, pp. 1656-1665.; C.L. Talcott, Symbolic modeling of signal transduction in Pathway Logic, in: L.F. Perrone, B. Lawson, J. Liu, F.P. Wieland (Eds.), Proceedings of the Winter Simulation Conference, WSC 2006, Monterey, California, USA, December 3-6, 2006, WSC, 2006, pp. 1656-1665.
[444] C.L. Talcott, Policy-based coordination in PAGODA: a case study, in: G. Boella, M. Dastani, A. Omicini, L. van der Torre, I. Cerna, I. Linden (Eds.), Combined Proceedings of the Second International Workshop on Coordination and Organization, CoOrg 2006, and the Second International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord 2006, Bologna, Italy, June 13, 2006, Electronic Notes in Theoretical Computer Science, vol. 181, Elsevier, 2007, pp. 97-112.; C.L. Talcott, Policy-based coordination in PAGODA: a case study, in: G. Boella, M. Dastani, A. Omicini, L. van der Torre, I. Cerna, I. Linden (Eds.), Combined Proceedings of the Second International Workshop on Coordination and Organization, CoOrg 2006, and the Second International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems, MTCoord 2006, Bologna, Italy, June 13, 2006, Electronic Notes in Theoretical Computer Science, vol. 181, Elsevier, 2007, pp. 97-112.
[445] C.L. Talcott, Pathway logic, in: M. Bernardo, P. Degano, G. Zavattaro (Eds.), Formal Methods for Computational Systems Biology, 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2008, Bertinoro, Italy, June 2-7, 2008, Advanced Lectures, Lecture Notes in Computer Science, vol. 5016, Springer, 2008, pp. 21-53.; C.L. Talcott, Pathway logic, in: M. Bernardo, P. Degano, G. Zavattaro (Eds.), Formal Methods for Computational Systems Biology, 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2008, Bertinoro, Italy, June 2-7, 2008, Advanced Lectures, Lecture Notes in Computer Science, vol. 5016, Springer, 2008, pp. 21-53.
[446] C.L. Talcott, D.L. Dill, The pathway logic assistant, in: G. Plotkin (Ed.), Proceedings of the Third International Workshop on Computational Methods in Systems Biology, 2005, pp. 228-239.; C.L. Talcott, D.L. Dill, The pathway logic assistant, in: G. Plotkin (Ed.), Proceedings of the Third International Workshop on Computational Methods in Systems Biology, 2005, pp. 228-239.
[447] Talcott, C. L.; Dill, D. L., Multiple representations of biological processes, (Priami, C.; Plotkin, G. D., Transactions on Computational Systems Biology VI. Transactions on Computational Systems Biology VI, Lecture Notes in Computer Science, vol. 4220 (2006), Springer), 221-245
[448] C.L. Talcott, S. Eker, M. Knapp, P. Lincoln, K. Laderoute, Pathway logic modeling of protein functional domains in signal transduction, in: R.B. Altman, A.K. Dunker, L. Hunter, T.A. Jung, T.E. Klein (Eds.), Proceedings of the 9th Pacific Symposium on Biocomputing, PSB 2004, Fairmont Orchid, Hawaii, USA, January 6-10, 2004, World Scientific, January 2004, pp. 568-580.; C.L. Talcott, S. Eker, M. Knapp, P. Lincoln, K. Laderoute, Pathway logic modeling of protein functional domains in signal transduction, in: R.B. Altman, A.K. Dunker, L. Hunter, T.A. Jung, T.E. Klein (Eds.), Proceedings of the 9th Pacific Symposium on Biocomputing, PSB 2004, Fairmont Orchid, Hawaii, USA, January 6-10, 2004, World Scientific, January 2004, pp. 568-580.
[449] S. Tang, Towards Secure Web Browsing, Ph.D. thesis, University of Illinois at Urbana-Champaign, 2011, 2011-05-25. Available from: <http://hdl.handle.net/2142/24307>; S. Tang, Towards Secure Web Browsing, Ph.D. thesis, University of Illinois at Urbana-Champaign, 2011, 2011-05-25. Available from: <http://hdl.handle.net/2142/24307>
[450] Thati, P.; Meseguer, J., Complete symbolic reachability analysis using back-and-forth narrowing, Theoretical Computer Science, 366, 1-2, 163-179 (2006) · Zbl 1110.68058
[451] P. Thati, K. Sen, N. Martı´-Oliet, An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0, in Gadducci and Montanari [205], pp. 261-281.; P. Thati, K. Sen, N. Martı´-Oliet, An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0, in Gadducci and Montanari [205], pp. 261-281. · Zbl 1272.68322
[452] S. Thorvaldsen, Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude, Master’s thesis, Department of Informatics, University of Oslo, June 2005.; S. Thorvaldsen, Modeling and Analysis of the OGDC Wireless Sensor Network Algorithm in Real-Time Maude, Master’s thesis, Department of Informatics, University of Oslo, June 2005.
[453] Tinelli, C., A DPLL-based calculus for ground satisfiability modulo theories, (Ianni, G.; Flesca, S., Proceedings of the 8th European Conference on Logics in Artificial Intelligence (Cosenza, Italy). Proceedings of the 8th European Conference on Logics in Artificial Intelligence (Cosenza, Italy), Lecture Notes in Artificial Intelligence, vol. 2424 (2002), Springer), 308-319 · Zbl 1013.68192
[454] A. Tiwari, C.L. Talcott, Analyzing a discrete model of aplysia central pattern generator, in: M. Heiner, A.M. Uhrmacher (Eds.), Computational Methods in Systems Biology, 6th International Conference, CMSB 2008, Rostock, Germany, October 12-15, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5307, Springer, 2008, pp. 347-366.; A. Tiwari, C.L. Talcott, Analyzing a discrete model of aplysia central pattern generator, in: M. Heiner, A.M. Uhrmacher (Eds.), Computational Methods in Systems Biology, 6th International Conference, CMSB 2008, Rostock, Germany, October 12-15, 2008, Proceedings, Lecture Notes in Computer Science, vol. 5307, Springer, 2008, pp. 347-366.
[455] A. Tiwari, C.L. Talcott, M. Knapp, P. Lincoln, K. Laderoute, Analyzing pathways using SAT-based approaches, in: H. Anai, K. Horimoto, T. Kutsia (Eds.), Algebraic Biology, Second International Conference, AB 2007, Castle of Hagenberg, Austria, July 2-4, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4545, Springer, 2007, pp. 155-169.; A. Tiwari, C.L. Talcott, M. Knapp, P. Lincoln, K. Laderoute, Analyzing pathways using SAT-based approaches, in: H. Anai, K. Horimoto, T. Kutsia (Eds.), Algebraic Biology, Second International Conference, AB 2007, Castle of Hagenberg, Austria, July 2-4, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4545, Springer, 2007, pp. 155-169. · Zbl 1126.92021
[456] Urbain, X., Modular & incremental automated termination proofs, Journal of Automated Reasoning, 32, 4, 315-355 (2004) · Zbl 1096.68076
[457] van Deursen, A.; Heering, J.; Klint, P., Language Prototyping: An Algebraic Specification Approach (1996), World Scientific · Zbl 0962.68114
[458] A. Verdejo, Building tools for LOTOS symbolic semantics in Maude, in: D. Peled, M.Y. Vardi, (Eds.), Formal Techniques for Networked and Distributed Systems - FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2529, Springer, 2002, pp. 292-307.; A. Verdejo, Building tools for LOTOS symbolic semantics in Maude, in: D. Peled, M.Y. Vardi, (Eds.), Formal Techniques for Networked and Distributed Systems - FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2529, Springer, 2002, pp. 292-307. · Zbl 1037.68516
[459] A. Verdejo, Maude como Marco Semántico Ejecutable, Ph.D. thesis, Facultad de Informática, Universidad Complutense de Madrid, Spain, March 2003.; A. Verdejo, Maude como Marco Semántico Ejecutable, Ph.D. thesis, Facultad de Informática, Universidad Complutense de Madrid, Spain, March 2003.
[460] 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
[461] 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
[462] Verdejo, A.; Pita, I.; Martı´-Oliet, N., Specification and verification of the tree identify protocol of IEEE 1394 in rewriting logic, Formal Aspects of Computing, 14, 3, 228-246 (2003) · Zbl 1029.68023
[463] P. Viry, La RéÉcriture Concurrente, Ph.D. thesis, Université de Nancy I, 1992.; P. Viry, La RéÉcriture Concurrente, Ph.D. thesis, Université de Nancy I, 1992.
[464] P. Viry, Rewriting: an effective model of concurrency, in: C. Halatsis, D.G. Maritsas, G. Philokyprou, S. Theodoridis, (Eds.), PARLE’94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings, Lecture Notes in Computer Science, vol. 817, Springer, 1994, pp. 648-660.; P. Viry, Rewriting: an effective model of concurrency, in: C. Halatsis, D.G. Maritsas, G. Philokyprou, S. Theodoridis, (Eds.), PARLE’94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings, Lecture Notes in Computer Science, vol. 817, Springer, 1994, pp. 648-660.
[465] P. Viry, Input/output for ELAN, in Meseguer [317], pp. 51-64.; P. Viry, Input/output for ELAN, in Meseguer [317], pp. 51-64.
[466] P. Viry, Adventures in sequent calculus modulo equations, in Kirchner and Kirchner [262], pp. 21-32.; P. Viry, Adventures in sequent calculus modulo equations, in Kirchner and Kirchner [262], pp. 21-32. · Zbl 0917.68100
[467] Viry, P., Equational rules for rewriting logic, Theoretical Computer Science, 285, 2, 487-517 (2002) · Zbl 1001.68058
[468] E. Visser, Program transformation with Stratego/XT: rules, strategies, tools, and systems in Stratego/XT 0.9, in: C. Lengauer, D.S. Batory, C. Consel, M. Odersky, (Eds.), Domain-Specific Program Generation, International Seminar, Dagstuhl Castle, Germany, March 23-28, 2003, Revised Papers, Lecture Notes in Computer Science, vol. 3016, Springer, 2004, pp. 216-238.; E. Visser, Program transformation with Stratego/XT: rules, strategies, tools, and systems in Stratego/XT 0.9, in: C. Lengauer, D.S. Batory, C. Consel, M. Odersky, (Eds.), Domain-Specific Program Generation, International Seminar, Dagstuhl Castle, Germany, March 23-28, 2003, Revised Papers, Lecture Notes in Computer Science, vol. 3016, Springer, 2004, pp. 216-238.
[469] L. Wang, Z. Kalbarczyk, R.K. Iyer, Formalizing system behavior for evaluating a system hang detector, in: Proceedings of the 27th IEEE Symposium on Reliable Distributed Systems, SRDS 2008, Napoli, Italy, October 6-8, 2008, IEEE, 2008, pp. 269-278.; L. Wang, Z. Kalbarczyk, R.K. Iyer, Formalizing system behavior for evaluating a system hang detector, in: Proceedings of the 27th IEEE Symposium on Reliable Distributed Systems, SRDS 2008, Napoli, Italy, October 6-8, 2008, IEEE, 2008, pp. 269-278.
[470] Wehrman, I.; Kitchin, D.; Cook, W. R.; Misra, J., A timed semantics of Orc, Theoretical Computer Science, 402, 2-3, 234-248 (2008) · Zbl 1147.68436
[471] J.M. Wing, J. Woodcock, J. Davies, (Eds.), FM’99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume II, Lecture Notes in Computer Science, vol. 1709, Springer, 1999.; J.M. Wing, J. Woodcock, J. Davies, (Eds.), FM’99 - Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings, Volume II, Lecture Notes in Computer Science, vol. 1709, Springer, 1999. · Zbl 0929.00076
[472] M. Wirsing, G. Denker, C.L. Talcott, A. Poggio, L. Briesemeister, A rewriting logic framework for soft constraints, in Denker and Talcott [139], pp. 181-197.; M. Wirsing, G. Denker, C.L. Talcott, A. Poggio, L. Briesemeister, A rewriting logic framework for soft constraints, in Denker and Talcott [139], pp. 181-197. · Zbl 1279.68124
[473] M. Wirsing, A. Knapp, A formal approach to object-oriented software engineering, in Meseguer [317], pp. 322-360.; M. Wirsing, A. Knapp, A formal approach to object-oriented software engineering, in Meseguer [317], pp. 322-360. · Zbl 1001.68024
[474] Wirsing, M.; Knapp, A., A formal approach to object-oriented software engineering, Theoretical Computer Science, 285, 2, 519-560 (2002) · Zbl 1001.68024
[475] Younes, H. L.S.; Simmons, R. G., Statistical probabilistic model checking with a focus on time-bounded properties, Information and Computation, 204, 9, 1368-1409 (2006) · Zbl 1110.68077
[476] M. Zhang, K. Ogata, M. Nakamura, Specification translation of state machines from equational theories into rewrite theories, in Dong and Zhu [143], pp. 678-693.; M. Zhang, K. Ogata, M. Nakamura, Specification translation of state machines from equational theories into rewrite theories, in Dong and Zhu [143], pp. 678-693.
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.