{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T04:44:37Z","timestamp":1778215477409,"version":"3.51.4"},"publisher-location":"Cham","reference-count":85,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031433443","type":"print"},{"value":"9783031433450","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-43345-0_1","type":"book-chapter","created":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T22:01:49Z","timestamp":1697925709000},"page":"3-24","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Building Correct-by-Construction Systems with\u00a0Formal Patterns"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"issue":"1","key":"1_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73\u2013132 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R., Hoang, T.S.: Using Design Patterns in Formal Methods: An Event-B Approach. In: Fitzgerald, J.S., Haxthausen, A.E., Yenig\u00fcn, H. (eds.) ICTAC. LNCS, vol. 5160, pp. 1\u20132. Springer (2008)","DOI":"10.1007\/978-3-540-85762-4_1"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Agha, G.: Actors. MIT Press (1986)","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/88.218170","volume":"1","author":"G Agha","year":"1993","unstructured":"Agha, G., Frolund, S., Panwar, R., Sturman, D.: A linguistic framework for dynamic composition of dependability protocols. IEEE Parall. Distrib. Technol.: Syst. Appl. 1, 3\u201314 (1993)","journal-title":"IEEE Parall. Distrib. Technol.: Syst. Appl."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018)","DOI":"10.1145\/3158668"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Agha, G.A., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci. 153(2) (2006)","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/3-540-60973-3_108","volume-title":"FME\u201996: Industrial Benefit and Advances in Formal Methods","author":"PSC Alencar","year":"1996","unstructured":"Alencar, P.S.C., Cowan, D.D., Lucena, C.J.P.: A formal approach to architectural design patterns. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 576\u2013594. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60973-3_108"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Alpuente, M., Cuenca-Ortega, A., Escobar, S., Meseguer, J.: A partial evaluation framework for order-sorted equational programs modulo axioms. J. Log. Algebraic Methods Program. 110, 100501 (2020)","DOI":"10.1016\/j.jlamp.2019.100501"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-642-22944-2_28","volume-title":"Algebra and Coalgebra in Computer Science","author":"M AlTurki","year":"2011","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386\u2013392. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22944-2_28"},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.02.069","volume":"234","author":"M AlTurki","year":"2009","unstructured":"AlTurki, M., Meseguer, J., Gunter, C.: Probabilistic modeling and analysis of DoS protection for the ASV protocol. Electr. Notes Theor. Comput. Sci. 234, 3\u201318 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"1_CR11","unstructured":"Bae, K., Escobar, S., Meseguer, J.: Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In: Rewriting Techniques and Applications (RTA\u201913). LIPIcs, vol. 21, pp. 81\u201396. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013)"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.scico.2014.09.011","volume":"103","author":"K Bae","year":"2015","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.C.: Designing and verifying distributed cyber-physical systems using multirate PALS: an airplane turning control system case study. Sci. Comput. Program. 103, 13\u201350 (2015)","journal-title":"Sci. Comput. Program."},{"key":"1_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2013.09.010","volume":"91","author":"K Bae","year":"2014","unstructured":"Bae, K., Meseguer, J., \u00d6lveczky, P.C.: Formal patterns for multirate distributed real-time systems. Sci. Comput. Program. 91, 3\u201344 (2014)","journal-title":"Sci. Comput. Program."},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-319-06410-9_7","volume-title":"FM 2014: Formal Methods","author":"K Bae","year":"2014","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 94\u2013109. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_7"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-10003-2_61","volume-title":"Automata, Languages and Programming","author":"JA Bergstra","year":"1980","unstructured":"Bergstra, J.A., Tucker, J.V.: A characterisation of computable data types by means of a finite equational specification method. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 76\u201390. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10003-2_61"},{"issue":"1\u20133","key":"1_CR16","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-10007-5_41","volume-title":"Abstract Software Specifications","author":"RM Burstall","year":"1980","unstructured":"Burstall, R.M., Goguen, J.A.: The semantics of clear, a specification language. In: Bj\u00f8orner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 292\u2013332. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10007-5_41"},{"key":"1_CR18","unstructured":"Buschmann, F., Meunier, R., Rohnert, H., Sommerlad, P.: Pattern-Oriented Software Architecture, Volume 1: A System of Patterns. Addison-Wesley (1996)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-68863-1_4","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"R Chadha","year":"2008","unstructured":"Chadha, R., Gunter, C.A., Meseguer, J., Shankesi, R., Viswanathan, M.: Modular preservation of safety properties by cookie-based DoS-protection wrappers. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 39\u201358. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_4"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"1_CR22","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2006.12.009","volume":"373","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Meseguer, J., Palomino, M.: Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. Theoret. Comput. Sci. 373, 70\u201391 (2007)","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"1_CR23","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction=i-axiomatization+first-order consistency. Inf. Comput. 159(1\u20132), 151\u2013186 (2000)","journal-title":"Inf. Comput."},{"issue":"4","key":"1_CR24","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-39953-4_1","volume-title":"Generic Programming","author":"JC Dehnert","year":"2000","unstructured":"Dehnert, J.C., Stepanov, A.: Fundamentals of generic programming. In: Jazayeri, M., Loos, R.G.K., Musser, D.R. (eds.) Generic Programming. LNCS, vol. 1766, pp. 1\u201311. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-39953-4_1"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Denker, G., Meseguer, J., Talcott, C.: Rewriting semantics of meta-objects and composable distributed services. ENTCS 36, Elsevier (2000). In: Proceedings of the 3rd International Workshop on Rewriting Logic and its Applications (2000)","DOI":"10.1016\/S1571-0661(05)80132-X"},{"issue":"11","key":"1_CR27","doi-asserted-by":"publisher","first-page":"1755","DOI":"10.1016\/j.jss.2007.03.005","volume":"80","author":"J Dong","year":"2007","unstructured":"Dong, J., Alencar, P.S.C., Cowan, D.D., Yang, S.: Composing pattern-based components and verifying correctness. J. Syst. Softw. 80(11), 1755\u20131769 (2007)","journal-title":"J. Syst. Softw."},{"key":"1_CR28","unstructured":"Dur\u00e1n, F.: A reflective module algebra with applications to the Maude language (1999), Ph.D. Thesis, University of M\u00e1laga"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110, 100497 (2020)","DOI":"10.1016\/j.jlamp.2019.100497"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Equational unification and matching, and symbolic reachability analysis in maude 3.2 (system description). In: Automated Reasoning - 11th International Joint Conference, IJCAR 2022. Lecture Notes in Computer Science, vol. 13385, pp. 529\u2013540. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_31","DOI":"10.1007\/978-3-031-10769-6_31"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-04222-5_15","volume-title":"Frontiers of Combining Systems","author":"F Dur\u00e1n","year":"2009","unstructured":"Dur\u00e1n, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 246\u2013262. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_15"},{"issue":"2","key":"1_CR32","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2006.07.002","volume":"66","author":"F Dur\u00e1n","year":"2007","unstructured":"Dur\u00e1n, F., Meseguer, J.: Maude\u2019s module algebra. Sci. Comput. Program. 66(2), 125\u2013153 (2007)","journal-title":"Sci. Comput. Program."},{"key":"1_CR33","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.jlap.2011.12.004","volume":"81","author":"F Dur\u00e1n","year":"2012","unstructured":"Dur\u00e1n, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Algebraic Logic Programm. 81, 816\u2013850 (2012)","journal-title":"J. Algebraic Logic Programm."},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-28872-2_6","volume-title":"Fundamental Approaches to Software Engineering","author":"J Eckhardt","year":"2012","unstructured":"Eckhardt, J., M\u00fchlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78\u201393. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_6"},{"key":"1_CR35","unstructured":"Eden, A.H., Hirshfeld, Y.: Principles in formal specification of object oriented design and architecture. In: Stewart, D.A., Johnson, J.H. (eds.) CASCON. p. 3. IBM (2001)"},{"key":"1_CR36","first-page":"103","volume":"39","author":"H Ehrig","year":"1989","unstructured":"Ehrig, H., Cla\u00dfen, I.: Overview of algebraic specification languages, environments and tools, and algebraic specification of software systems. Bull. Europ. Assoc. Theor. Comput. Sci. 39, 103\u2013111 (1989)","journal-title":"Bull. Europ. Assoc. Theor. Comput. Sci."},{"key":"1_CR37","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Algebraic Logic Program. 81, 898\u2013928 (2012)","journal-title":"J. Algebraic Logic Program."},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific (1998)","DOI":"10.1142\/3831"},{"key":"1_CR39","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Elements of Reusable Object-Oriented Software. John Wiley & Sons (1994)"},{"key":"1_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-10009-1_27","volume-title":"5th Conference on Automated Deduction Les Arcs, France, July 8\u201311, 1980","author":"JA Goguen","year":"1980","unstructured":"Goguen, J.A.: How to prove algebraic inductive hypotheses without induction. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 356\u2013373. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10009-1_27"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action, pp. 3\u2013167. Kluwer (2000)","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Grimmett, G., Stirzaker, D.: Probability and Random Processes (3rd, Ed.). Oxford University Press (2001)","DOI":"10.1093\/oso\/9780198572237.001.0001"},{"key":"1_CR43","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/j.scico.2014.07.003","volume":"99","author":"R Guti\u00e9rrez","year":"2015","unstructured":"Guti\u00e9rrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. Sci. Comput. Program. 99, 235\u2013261 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"1_CR44","doi-asserted-by":"publisher","first-page":"553","DOI":"10.14778\/3055540.3055548","volume":"10","author":"R Harding","year":"2017","unstructured":"Harding, R., Aken, D.V., Pavlo, A., Stonebraker, M.: An evaluation of distributed concurrency control. Proc. VLDB Endow. 10(5), 553\u2013564 (2017)","journal-title":"Proc. VLDB Endow."},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Kiczales, G., Mezini, M.: Aspect-oriented programming and modular reasoning. In: 27th International Conference on Software Engineering ICSE 2005, pp. 49\u201358. ACM (2005)","DOI":"10.1145\/1062455.1062482"},{"key":"1_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Liu, S., Meseguer, J., \u00d6lveczky, P.C., Zhang, M., Basin, D.: Bridging the semantic gap between qualitative and quantitative models of distributed systems 6(OOPSLA2) (2022). https:\/\/doi.org\/10.1145\/3563299","DOI":"10.1145\/3563299"},{"issue":"5","key":"1_CR48","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/s00165-019-00489-w","volume":"31","author":"S Liu","year":"2019","unstructured":"Liu, S., \u00d6lveczky, P.C., Wang, Q., Gupta, I., Meseguer, J.: Read atomic transactions with prevention of lost updates: ROLA and its formal analysis. Formal Aspects Comput. 31(5), 503\u2013540 (2019)","journal-title":"Formal Aspects Comput."},{"key":"1_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-030-17465-1_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Liu","year":"2019","unstructured":"Liu, S., \u00d6lveczky, P.C., Zhang, M., Wang, Q., Meseguer, J.: Automatic analysis of consistency properties of distributed transaction systems in Maude. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 40\u201357. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_3"},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-55754-6_2","volume-title":"NASA Formal Methods","author":"S Liu","year":"2020","unstructured":"Liu, S., Sandur, A., Meseguer, J., \u00d6lveczky, P.C., Wang, Q.: Generating Correct-by-Construction Distributed Implementations from Formal Maude Designs. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 22\u201340. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_2"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Algebraic simulations. J. Log. Algebr. Program 79(2), 103\u2013143 (2010)","DOI":"10.1016\/j.jlap.2009.07.003"},{"key":"1_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-030-63595-4_7","volume-title":"Rewriting Logic and Its Applications","author":"J Meseguer","year":"2020","unstructured":"Meseguer, J., Skeirik, S.: Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 114\u2013135. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_7"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-47993-7_1","volume-title":"ECOOP 2002 \u2014 Object-Oriented Programming","author":"J Meseguer","year":"2002","unstructured":"Meseguer, J., Talcott, C.: Semantic models for distributed object reflection. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 1\u201336. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-47993-7_1"},{"issue":"1\u20132","key":"1_CR54","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10990-007-9000-6","volume":"20","author":"J Meseguer","year":"2007","unstructured":"Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to the verification of cryptographic protocols. J. Higher-Order Symbol. Comput. 20(1\u20132), 123\u2013160 (2007)","journal-title":"J. Higher-Order Symbol. Comput."},{"issue":"1","key":"1_CR55","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P., Yonezawa, A. (eds.) Research Directions in Concurrent Object-Oriented Programming, pp. 314\u2013390. MIT Press (1993)","DOI":"10.7551\/mitpress\/2087.003.0017"},{"key":"1_CR57","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Algebraic Logic Programm. 81, 721\u2013781 (2012)","journal-title":"J. Algebraic Logic Programm."},{"key":"1_CR58","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2013.07.004","volume":"83","author":"J Meseguer","year":"2014","unstructured":"Meseguer, J.: Taming distributed system complexity through formal patterns. Sci. Comput. Program. 83, 3\u201334 (2014)","journal-title":"Sci. Comput. Program."},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program. 110, 100483 (2020)","DOI":"10.1016\/j.jlamp.2019.100483"},{"key":"1_CR60","doi-asserted-by":"publisher","unstructured":"Meseguer, J.: Checking sufficient completeness by inductive theorem proving. In: Rewriting Logic and Its Applications - 14th International Workshop, WRLA@ETAPS 2022. Lecture Notes in Computer Science, vol. 13252, pp. 171\u2013190. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-12441-9_9","DOI":"10.1007\/978-3-031-12441-9_9"},{"key":"1_CR61","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2012.05.040","volume":"451","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1\u201337 (2012)","journal-title":"Theor. Comput. Sci."},{"issue":"2\u20133","key":"1_CR62","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2008.04.040","volume":"403","author":"J Meseguer","year":"2008","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. Theoret. Comput. Sci. 403(2\u20133), 239\u2013264 (2008)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR63","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice Hall (1997)"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Mikkonen, T.: Formalizing design patterns. In: ICSE, pp. 115\u2013124 (1998)","DOI":"10.1109\/ICSE.1998.671108"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Miller, S., Cofer, D., Sha, L., Meseguer, J., Al-Nayeem, A.: Implementing logical synchrony in integrated modular avionics. In: Proceedings of the 28th Digital Avionics Systems Conference. IEEE (2009)","DOI":"10.1109\/DASC.2009.5347579"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"Misra, J.: A Discipline of Multiprogramming. Springer-Verlag (2001)","DOI":"10.1007\/978-1-4419-8528-6"},{"key":"1_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/b96103","volume-title":"Casl Reference Manual","year":"2004","unstructured":"Mosses, P.D. (ed.): Casl Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/b96103"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Musser, D.: On proving inductive properties of abstract data types. In: Proceedings, 7th Symposium on Principles of Programming Languages. Association for Computing Machinery (1980)","DOI":"10.1145\/567446.567461"},{"key":"1_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51084-2","volume-title":"Symbolic and Algebraic Computation","year":"1989","unstructured":"Gianni, P. (ed.): ISSAC 1988. LNCS, vol. 358. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51084-2"},{"key":"1_CR70","unstructured":"PRISM: PRISM-SMC (Accessed April 2022). https:\/\/www.prismmodelchecker.org\/manual\/RunningPRISM\/StatisticalModelChecking"},{"key":"1_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-22944-2_22","volume-title":"Algebra and Coalgebra in Computer Science","author":"C Rocha","year":"2011","unstructured":"Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., C\u00eerstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314\u2013328. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22944-2_22"},{"key":"1_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/978-3-642-54624-2_30","volume-title":"Specification, Algebra, and Software","author":"C Rocha","year":"2014","unstructured":"Rocha, C., Meseguer, J.: Mechanical analysis of reliable communication in the alternating bit protocol using the Maude invariant analyzer tool. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 603\u2013629. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54624-2_30"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"Rubinstein, R., Kroese, D.: Simulation and the Monte Carlo Method (3rd, Ed.). J. Wiley & Sons (2017)","DOI":"10.1002\/9781118631980"},{"key":"1_CR74","doi-asserted-by":"crossref","unstructured":"Saeki, M.: Behavioral specification of GOF design patterns with LOTOS. In: APSEC. pp. 408\u2013415. IEEE Computer Society (2000)","DOI":"10.1109\/APSEC.2000.896727"},{"key":"1_CR75","unstructured":"Schmidt, D., Stal, M., Rohnert, H., Buschmann, F.: Pattern-Oriented Software Architecture, Volume 2: Patterns for Concurrent and Networked Objects. John Wiley & Sons (2000)"},{"key":"1_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-030-63595-4_10","volume-title":"Rewriting Logic and Its Applications","author":"S Skeirik","year":"2020","unstructured":"Skeirik, S., Meseguer, J., Rocha, C.: Verification of the IBOS browser security properties in reachability logic. In: Escobar, S., Mart\u00ed-Oliet, N. (eds.) WRLA 2020. LNCS, vol. 12328, pp. 176\u2013196. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63595-4_10"},{"issue":"4","key":"1_CR77","doi-asserted-by":"publisher","first-page":"315","DOI":"10.3233\/FI-2020-1926","volume":"173","author":"S Skeirik","year":"2020","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Fundam. Inform. 173(4), 315\u2013382 (2020)","journal-title":"Fundam. Inform."},{"key":"1_CR78","doi-asserted-by":"crossref","unstructured":"Soundarajan, N., Hallstrom, J.O.: Responsibilities and rewards: Specifying design patterns. In: ICSE, pp. 666\u2013675. IEEE Computer Society (2004)","DOI":"10.1109\/ICSE.2004.1317488"},{"key":"1_CR79","doi-asserted-by":"crossref","unstructured":"Sun, M., Meseguer, J.: Distributed real-time emulation of formally-defined patterns for safe medical device control. In: \u00d6lveczky, P.C. (ed.) Proceedings of the 1st International Workshop on Rewriting Techniques for Real-Time Systems, RTRTS 2010. Electronic Proceedings in Theoretical Computer Science, vol. 36, pp. 158\u2013177 (2010)","DOI":"10.4204\/EPTCS.36.9"},{"key":"1_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-319-12904-4_15","volume-title":"Rewriting Logic and Its Applications","author":"M Sun","year":"2014","unstructured":"Sun, M., Meseguer, J.: Formal specification of button-related fault-tolerance micropatterns. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 263\u2013279. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12904-4_15"},{"key":"1_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-16310-4_11","volume-title":"Rewriting Logic and Its Applications","author":"M Sun","year":"2010","unstructured":"Sun, M., Meseguer, J., Sha, L.: A formal pattern architecture for safe medical systems. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 157\u2013173. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16310-4_11"},{"issue":"4","key":"1_CR82","doi-asserted-by":"publisher","first-page":"127","DOI":"10.5381\/jot.2003.2.4.a4","volume":"2","author":"T Taibi","year":"2003","unstructured":"Taibi, T., Ling, D.N.C.: Formal specification of design patterns - a balanced approach. J. Object Technol. 2(4), 127\u2013140 (2003)","journal-title":"J. Object Technol."},{"issue":"1","key":"1_CR83","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/1005561.1005564","volume":"13","author":"N Venkatasubramanian","year":"2004","unstructured":"Venkatasubramanian, N., Talcott, C.L., Agha, G.: A formal model for reasoning about adaptive QoS-enabled middleware. ACM Trans. Softw. Eng. Methodol. 13(1), 86\u2013147 (2004)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1_CR84","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoret. Comput. Sci. 285, 487\u2013517 (2002)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"835","DOI":"10.1007\/3-540-48224-5_68","volume-title":"Automata, Languages and Programming","author":"M Viswanathan","year":"2001","unstructured":"Viswanathan, M., Viswanathan, R.: Foundations for circular compositional reasoning. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 835\u2013847. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-48224-5_68"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43345-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T16:03:56Z","timestamp":1730390636000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43345-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433443","9783031433450"],"references-count":85,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43345-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WADT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Algebraic Development Techniques","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 June 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 June 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"adt2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/wadt2022.web.ua.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}