TY - GEN
T1 - Symbolic Computation in Maude
T2 - 30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020
AU - Meseguer, José
N1 - Funding Information:
Acknowledgements. I thank the BOPL organizers for giving me the opportunity of presenting these ideas as a BOPL joint invited speaker. I chose the talk’s topic having in mind the interests of the various BOPL participants and, in spite of the pandemic, found the online discussions very helpful and stimulating. The ideas I have presented are based on joint work with various colleagues. The symbolic aspects of Maude are part of a long and extremely active effort by the members of the Maude Team; they owe much to Steven Eker’s high-performance implementation of its features. Folding variant narrowing is joint work with Santiago Escobar and Ralf Sasse. Variant-based satisfiability has been advanced in joint work with Stephen Skeirik and Raúl Gutiérrez. The Maude-NPA has been developed in joint work with Catherine Meadows, Santiago Escobar, and Ph.D. students at Illinois, Valencia, and Oslo. Maude’s Symbolic LTL Model Checker is joint work with Kyungmin Bae and Santiago Escobar. Last but not least, the work on generalization, homeomorphic embedding and variant-based partial evaluation of Maude programs is joint research with María Alpuente, Angel Cuenca-Ortega, Santiago Escobar and Julia Sapiña at TU Valencia, and Demis Ballis at the University of Udine. Given the long list, I hope I have not missed anybody, and apologize in advance if that were inadvertently the case. I warmly thank María Alpuente, Francisco Durán, Santiago Escobar, Maribel Fernádez, Salvador Lucas, Narciso Martí-Oliet, Rubén Rubio and Carolyn Talcott for their very helpful suggestions to improve the manuscript. The research reported herein has been partially supported by NRL under contract N00173-17-1-G002.
Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - Programming in Maude is executable mathematical modeling. Your mathematical model is the code you execute. Both deterministic systems, specified equationally as so-called functional modules and concurrent ones, specified in rewriting logic as system modules, are mathematically modeled and programmed this way. But rewriting logic is also a logical framework in which many different logics can be naturally represented. And one would like not only to execute these models, but to reason about them at a high level. For this, symbolic methods that can automate much of the reasoning are crucial. Many of them are actually supported by Maude itself or by some of its tools. These methods are very general: they apply not just to Maude, but to many other logics, languages and tools. This paper presents some tapas about these Maude-based symbolic methods in an informal way to make it easy for many other people to learn about, and benefit from, them.
AB - Programming in Maude is executable mathematical modeling. Your mathematical model is the code you execute. Both deterministic systems, specified equationally as so-called functional modules and concurrent ones, specified in rewriting logic as system modules, are mathematically modeled and programmed this way. But rewriting logic is also a logical framework in which many different logics can be naturally represented. And one would like not only to execute these models, but to reason about them at a high level. For this, symbolic methods that can automate much of the reasoning are crucial. Many of them are actually supported by Maude itself or by some of its tools. These methods are very general: they apply not just to Maude, but to many other logics, languages and tools. This paper presents some tapas about these Maude-based symbolic methods in an informal way to make it easy for many other people to learn about, and benefit from, them.
UR - http://www.scopus.com/inward/record.url?scp=85102621841&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85102621841&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-68446-4_1
DO - 10.1007/978-3-030-68446-4_1
M3 - Conference contribution
AN - SCOPUS:85102621841
SN - 9783030684457
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 3
EP - 36
BT - Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings
A2 - Fernández, Maribel
PB - Springer
Y2 - 7 September 2020 through 9 September 2020
ER -