Difference between revisions of "Some Papers on Maude and on Rewriting Logic"
From The Maude System
| Line 3: | Line 3: | ||
In-depth presentations of Maude, and on how to use its most common features, are available in the following books: | In-depth presentations of Maude, and on how to use its most common features, are available in the following books: | ||
| − | * M. Clavel | + | * M. Clavel et al.: [https://doi.org/10.1007/978-3-540-71999-1 All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic]. LNCS 4350, Springer (2007) |
* P.C. Ölveczky: [https://doi.org/10.1007/978-1-4471-6687-0 Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude]. Springer (2017) | * P.C. Ölveczky: [https://doi.org/10.1007/978-1-4471-6687-0 Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude]. Springer (2017) | ||
| Line 9: | Line 9: | ||
Several bibliographies and surveys on rewriting logic and Maude have been published: | Several bibliographies and surveys on rewriting logic and Maude have been published: | ||
| − | * M. Clavel | + | * M. Clavel et al.: [https://doi.org/10.1007/978-3-319-23165-5_11 Two Decades of Maude]. Logic, Rewriting, and Concurrency: 232-254 (2015). A pre-print is available [[Media:Two-Decades-of-Maude.pdf|here]]. |
* J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.06.003 Twenty years of rewriting logic]. J. Log. Algebraic Methods Program. 81(7-8): 721-781 (2012). A pre-print is available [[Media:20-years.pdf|here]]. | * J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.06.003 Twenty years of rewriting logic]. J. Log. Algebraic Methods Program. 81(7-8): 721-781 (2012). A pre-print is available [[Media:20-years.pdf|here]]. | ||
| − | * N. Martí-Oliet, M. Palomino, A. Verdejo: [https://www.sciencedirect.com/science/article/pii/S1567832612000562?via%3Dihub Rewriting logic bibliography by topic: 1990–2011]. J. Log. Algebraic Methods Program. 81: 782-815 (2012) | + | * N. Martí-Oliet, M. Palomino, and A. Verdejo: [https://www.sciencedirect.com/science/article/pii/S1567832612000562?via%3Dihub Rewriting logic bibliography by topic: 1990–2011]. J. Log. Algebraic Methods Program. 81: 782-815 (2012) |
| − | * N. Martí-Oliet | + | * N. Martí-Oliet and J. Meseguer: [https://www.sciencedirect.com/science/article/pii/S0304397501003577 Rewriting logic: roadmap and bibliography]. Theor. Comput. Sci. 285(2): 121-154 (2002). A pre-print is available [[Media:MMroadmap_2001.pdf|here]]. |
The following papers may serve as a selection of such huge body of work: | The following papers may serve as a selection of such huge body of work: | ||
| − | * F. Durán | + | * F. Durán et al.: [https://doi.org/10.1016/j.jlamp.2019.100497 Programming and symbolic computation in Maude]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:maude-jlamp.pdf|here]]. |
* J. Meseguer: [https://doi.org/10.1016/j.jlamp.2019.100483 Generalized rewrite theories, coherence completion, and symbolic methods]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:BMgrt_2003.pdf|here]]. | * J. Meseguer: [https://doi.org/10.1016/j.jlamp.2019.100483 Generalized rewrite theories, coherence completion, and symbolic methods]. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available [[Media:BMgrt_2003.pdf|here]]. | ||
| − | * F. Durán, J. Meseguer, C. Rocha: [https://doi.org/10.1016/j.jlamp.2019.100513 Ground confluence of order-sorted conditional specifications modulo axioms]. J. Log. Algebraic Methods Program. 111: 100513 (2020). A pre-print is available [[Media:Durán.Mesegue.Rocha.Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms.TR.pdf|here]]. | + | * F. Durán, J. Meseguer, and C. Rocha: [https://doi.org/10.1016/j.jlamp.2019.100513 Ground confluence of order-sorted conditional specifications modulo axioms]. J. Log. Algebraic Methods Program. 111: 100513 (2020). A pre-print is available [[Media:Durán.Mesegue.Rocha.Ground Confluence of Order-sorted Conditional Specifications Modulo Axioms.TR.pdf|here]]. |
* C. Rocha, J. Meseguer, C. Muñoz: [https://doi.org/10.1016/j.jlamp.2016.10.001 Rewriting modulo SMT and open system analysis]. J. Log. Algebraic Methods Program. 86(1): 269-297 (2017) | * C. Rocha, J. Meseguer, C. Muñoz: [https://doi.org/10.1016/j.jlamp.2016.10.001 Rewriting modulo SMT and open system analysis]. J. Log. Algebraic Methods Program. 86(1): 269-297 (2017) | ||
| Line 29: | Line 29: | ||
* S. Escobar, R. Sasse, J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.01.002 Folding variant narrowing and optimal variant termination]. J. Log. Algebraic Methods Program. 81(7-8): 898-928 (2012) | * S. Escobar, R. Sasse, J. Meseguer: [https://doi.org/10.1016/j.jlap.2012.01.002 Folding variant narrowing and optimal variant termination]. J. Log. Algebraic Methods Program. 81(7-8): 898-928 (2012) | ||
| − | * F. Durán | + | * F. Durán and J. Meseguer: [https://doi.org/10.1016/j.jlap.2011.12.004 On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories]. J. Log. Algebraic Methods Program. 81(7-8): 816-850 (2012). A pre-print is available [[Media:CRChC.pdf|here]]. |
| − | * J. Meseguer, M. Palomino, N. Martí-Oliet: [https://doi.org/10.1016/j.jlap.2009.07.003 Algebraic simulations]. J. Log. Algebraic Methods Program. 79(2): 103-143 (2010). A pre-print is available [[Media:MartiOlietEtAl03-journal.pdf|here]]. | + | * J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.jlap.2009.07.003 Algebraic simulations]. J. Log. Algebraic Methods Program. 79(2): 103-143 (2010). A pre-print is available [[Media:MartiOlietEtAl03-journal.pdf|here]]. |
| − | * J. Meseguer, M. Palomino, N. Martí-Oliet: [https://doi.org/10.1016/j.tcs.2008.04.040 Equational abstractions]. Theor. Comput. Sci. 403(2-3): 239-264 (2008). A pre-print is available [[Media:MPMea_2003.pdf|here]]. | + | * J. Meseguer, M. Palomino, and N. Martí-Oliet: [https://doi.org/10.1016/j.tcs.2008.04.040 Equational abstractions]. Theor. Comput. Sci. 403(2-3): 239-264 (2008). A pre-print is available [[Media:MPMea_2003.pdf|here]]. |
| − | * M. Clavel, J. Meseguer, M. Palomino: [https://doi.org/10.1016/j.tcs.2006.12.009 Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic]. Theor. Comput. Sci. 373(1-2): 70-91 (2007) | + | * M. Clavel, J. Meseguer, and M. Palomino: [https://doi.org/10.1016/j.tcs.2006.12.009 Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic]. Theor. Comput. Sci. 373(1-2): 70-91 (2007) |
| − | * P.C. Ölveczky | + | * P.C. Ölveczky and J. Meseguer: [https://doi.org/10.1007/s10990-007-9001-5 Semantics and pragmatics of Real-Time Maude]. High. Order Symb. Comput. 20(1-2): 161-196 (2007) |
| − | * F. Durán | + | * F. Durán and J. Meseguer: [https://doi.org/10.1016/j.scico.2006.07.002 Maude's module algebra]. Sci. Comput. Program. 66(2): 125-153 (2007) |
| − | * R. Bruni | + | * R. Bruni and J. Meseguer: [https://doi.org/10.1016/j.tcs.2006.04.012 Semantic foundations for generalized rewrite theories]. Theor. Comput. Sci. 360(1-3): 386-414 (2006) |
| − | * M. Clavel | + | * M. Clavel et al.: [https://doi.org/10.1016/S0304-3975(01)00359-0 Maude: specification and programming in rewriting logic]. Theor. Comput. Sci. 285(2): 187-243 (2002). A pre-print is available [[Media:CDELMMQspecprog_2001.pdf|here]]. |
* J. Meseguer: [https://doi.org/10.1007/3-540-64299-4_26 Membership algebra as a logical framework for equational specification]. WADT: 18-61 (1997) | * J. Meseguer: [https://doi.org/10.1007/3-540-64299-4_26 Membership algebra as a logical framework for equational specification]. WADT: 18-61 (1997) | ||
| − | * N. Martí-Oliet | + | * N. Martí-Oliet and J. Meseguer: [https://doi.org/10.1016/S1571-0661(04)00040-4 Rewriting logic as a logical and semantic framework]. WRLA: 190-225 (1996) |
* J. Meseguer: [https://www.sciencedirect.com/science/article/pii/030439759290182F Conditional rewriting logic as a unified model of concurrency]. Theor. Comput. Sci. 96(1): 73-155 (1996) | * J. Meseguer: [https://www.sciencedirect.com/science/article/pii/030439759290182F Conditional rewriting logic as a unified model of concurrency]. Theor. Comput. Sci. 96(1): 73-155 (1996) | ||
| + | |||
| + | Some interesting applications and uses of Maude: | ||
| + | |||
| + | * S. Liu et al.: [https://dl.acm.org/doi/abs/10.1145/3603269.3604870 A Formal Framework for End-to-End DNS Resolution]. ACM SIGCOMM, pages 932–949 (2023) | ||
| + | |||
| + | * S. Liu et al.: [https://doi.org/10.1145/3563299 Bridging the semantic gap between qualitative and quantitative models of distributed systems]. Proc. ACM Program. Lang. 6(OOPSLA2): 315-344 (2022) | ||
| + | |||
| + | * P. Meredith et al. [doi: 10.1109/MEMCOD.2010.5558634 A formal executable semantics of Verilog] 8th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE) pp. 179-188 (2010) | ||
| + | |||
| + | * P.C. Ölveczky, A. Boronat, and J. Meseguer: [https://doi.org/10.1007/978-3-642-13464-7_5 Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude]. Formal Techniques for Distributed Systems (FORTE), LNCS 6117 (2010) | ||
| + | |||
| + | * S. Escobar, C. Meadows, and J. Meseguer: [https://doi.org/10.1007/978-3-642-03829-7_1 Maude-NPA: Cryptographic protocol analysis modulo equational properties] Foundations of Security Analysis and Design, LNCS 5705:1-50, Springer (2009) | ||
| + | |||
| + | * J.E. Rivera, F. Durán, and A. Vallecillo: [doi:10.1177/0037549709341635 Formal Specification and Analysis of Domain Specific Models Using Maude]. SIMULATION. 85(11-12):778-792 (2009) | ||
| + | |||
| + | * S. Chen et al.: [doi: 10.1109/SP.2007.6 A Systematic Approach to Uncover Security Flaws in GUI Logic] in IEEE Symposium on Security and Privacy (SP), pp. 71-85 (2007) | ||
| + | |||
| + | * J.R. Romero et al.: [doi:10.5381/jot.2007.6.9.a10 Formal and Tool Support for Model Driven Engineering with Maude], Journal of Object Technology 6(9):187-207 (2007) | ||
| + | |||
| + | * S. Escobar, C. Meadows, and J. Meseguer: [https://doi.org/10.1016/j.tcs.2006.08.035 A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties], TCS 367(1–2):162-202 (2006) | ||
| + | |||
| + | * P.C. Ölveczky, J. Meseguer, and C.L. Talcott [https://doi.org/10.1007/s10703-006-0015-0 Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude]. Form Method Syst Des 29, 253–293 (2006) | ||
| + | |||
| + | * G. Roşu and K. Havelund: [https://doi.org/10.1007/s10515-005-6205-y Rewriting-Based Techniques for Runtime Verification]. Autom Software Eng 12, 151–197 (2005) | ||
| + | |||
| + | * A. Farzan et al.: [https://doi.org/10.1007/978-3-540-27813-9_46 Formal Analysis of Java Programs in JavaFAN]. Computer Aided Verification (CAV). LNCS 3114 (2004) | ||
| + | |||
| + | * S. Eker et al.: [https://pubmed.ncbi.nlm.nih.gov/11928493/ Pathway logic: symbolic analysis of biological signaling]. Pac Symp Biocomput. 2002:400-12. (2002) | ||
| + | |||
| + | * P. Degano, J. Meseguer, and U. Montanari, [doi: 10.1109/LICS.1989.39172 Axiomatizing net computations and processes] Fourth Annual Symposium on Logic in Computer Science, pp. 175-185 (1989) | ||
Some Additional Papers on Maude and on Rewriting Logic are available [http://maude.cs.illinois.edu/papers/ here]. | Some Additional Papers on Maude and on Rewriting Logic are available [http://maude.cs.illinois.edu/papers/ here]. | ||
Revision as of 10:21, 11 December 2023
A friendly introduction to the latest advances in the symbolic features of Maude will appear in Proc. LOPSTER 2020: Symbolic Computation in Maude: Some Tapas.
In-depth presentations of Maude, and on how to use its most common features, are available in the following books:
- M. Clavel et al.: All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS 4350, Springer (2007)
- P.C. Ölveczky: Designing Reliable Distributed Systems - A Formal Methods Approach Based on Executable Modeling in Maude. Springer (2017)
Several bibliographies and surveys on rewriting logic and Maude have been published:
- M. Clavel et al.: Two Decades of Maude. Logic, Rewriting, and Concurrency: 232-254 (2015). A pre-print is available here.
- J. Meseguer: Twenty years of rewriting logic. J. Log. Algebraic Methods Program. 81(7-8): 721-781 (2012). A pre-print is available here.
- N. Martí-Oliet, M. Palomino, and A. Verdejo: Rewriting logic bibliography by topic: 1990–2011. J. Log. Algebraic Methods Program. 81: 782-815 (2012)
- N. Martí-Oliet and J. Meseguer: Rewriting logic: roadmap and bibliography. Theor. Comput. Sci. 285(2): 121-154 (2002). A pre-print is available here.
The following papers may serve as a selection of such huge body of work:
- F. Durán et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available here.
- J. Meseguer: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program. 110 (2020). A pre-print is available here.
- F. Durán, J. Meseguer, and C. Rocha: Ground confluence of order-sorted conditional specifications modulo axioms. J. Log. Algebraic Methods Program. 111: 100513 (2020). A pre-print is available here.
- C. Rocha, J. Meseguer, C. Muñoz: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86(1): 269-297 (2017)
- S. Escobar, R. Sasse, J. Meseguer: Folding variant narrowing and optimal variant termination. J. Log. Algebraic Methods Program. 81(7-8): 898-928 (2012)
- F. Durán and J. Meseguer: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebraic Methods Program. 81(7-8): 816-850 (2012). A pre-print is available here.
- J. Meseguer, M. Palomino, and N. Martí-Oliet: Algebraic simulations. J. Log. Algebraic Methods Program. 79(2): 103-143 (2010). A pre-print is available here.
- J. Meseguer, M. Palomino, and N. Martí-Oliet: Equational abstractions. Theor. Comput. Sci. 403(2-3): 239-264 (2008). A pre-print is available here.
- M. Clavel, J. Meseguer, and M. Palomino: Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic. Theor. Comput. Sci. 373(1-2): 70-91 (2007)
- P.C. Ölveczky and J. Meseguer: Semantics and pragmatics of Real-Time Maude. High. Order Symb. Comput. 20(1-2): 161-196 (2007)
- F. Durán and J. Meseguer: Maude's module algebra. Sci. Comput. Program. 66(2): 125-153 (2007)
- R. Bruni and J. Meseguer: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1-3): 386-414 (2006)
- M. Clavel et al.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2): 187-243 (2002). A pre-print is available here.
- J. Meseguer: Membership algebra as a logical framework for equational specification. WADT: 18-61 (1997)
- N. Martí-Oliet and J. Meseguer: Rewriting logic as a logical and semantic framework. WRLA: 190-225 (1996)
- J. Meseguer: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1): 73-155 (1996)
Some interesting applications and uses of Maude:
- S. Liu et al.: A Formal Framework for End-to-End DNS Resolution. ACM SIGCOMM, pages 932–949 (2023)
- S. Liu et al.: Bridging the semantic gap between qualitative and quantitative models of distributed systems. Proc. ACM Program. Lang. 6(OOPSLA2): 315-344 (2022)
- P. Meredith et al. [doi: 10.1109/MEMCOD.2010.5558634 A formal executable semantics of Verilog] 8th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE) pp. 179-188 (2010)
- P.C. Ölveczky, A. Boronat, and J. Meseguer: Formal Semantics and Analysis of Behavioral AADL Models in Real-Time Maude. Formal Techniques for Distributed Systems (FORTE), LNCS 6117 (2010)
- S. Escobar, C. Meadows, and J. Meseguer: Maude-NPA: Cryptographic protocol analysis modulo equational properties Foundations of Security Analysis and Design, LNCS 5705:1-50, Springer (2009)
- J.E. Rivera, F. Durán, and A. Vallecillo: [doi:10.1177/0037549709341635 Formal Specification and Analysis of Domain Specific Models Using Maude]. SIMULATION. 85(11-12):778-792 (2009)
- S. Chen et al.: [doi: 10.1109/SP.2007.6 A Systematic Approach to Uncover Security Flaws in GUI Logic] in IEEE Symposium on Security and Privacy (SP), pp. 71-85 (2007)
- J.R. Romero et al.: [doi:10.5381/jot.2007.6.9.a10 Formal and Tool Support for Model Driven Engineering with Maude], Journal of Object Technology 6(9):187-207 (2007)
- S. Escobar, C. Meadows, and J. Meseguer: A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties, TCS 367(1–2):162-202 (2006)
- P.C. Ölveczky, J. Meseguer, and C.L. Talcott Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. Form Method Syst Des 29, 253–293 (2006)
- G. Roşu and K. Havelund: Rewriting-Based Techniques for Runtime Verification. Autom Software Eng 12, 151–197 (2005)
- A. Farzan et al.: Formal Analysis of Java Programs in JavaFAN. Computer Aided Verification (CAV). LNCS 3114 (2004)
- S. Eker et al.: Pathway logic: symbolic analysis of biological signaling. Pac Symp Biocomput. 2002:400-12. (2002)
- P. Degano, J. Meseguer, and U. Montanari, [doi: 10.1109/LICS.1989.39172 Axiomatizing net computations and processes] Fourth Annual Symposium on Logic in Computer Science, pp. 175-185 (1989)
Some Additional Papers on Maude and on Rewriting Logic are available here.
