TY - JOUR
T1 - Programming and symbolic computation in Maude
AU - Durán, Francisco
AU - Eker, Steven
AU - Escobar, Santiago
AU - Martí-Oliet, Narciso
AU - Meseguer, José
AU - Rubio, Rubén
AU - Talcott, Carolyn
N1 - Funding Information:
Durán has been partially supported by MINECO/FEDER project TIN2014-52034-R . Escobar has been partially supported by the EU ( FEDER ) and the MCIU under grant RTI2018-094403-B-C32 , by the Spanish Generalitat Valenciana under grant PROMETEO/2019/098 , and by the US Air Force Office of Scientific Research under award number FA9550-17-1-0286 . Martí-Oliet and Rubio have been partially supported by MCIU Spanish project TRACES ( TIN2015-67522-C3-3-R ). Rubio has also been partially supported by a MCIU grant FPU17/02319 . Meseguer and Talcott have been partially supported by NRL Grant N00173-17-1-G002 . Talcott has also been partially supported by ONR Grant N00014-15-1-2202 .
PY - 2020/1
Y1 - 2020/1
N2 - Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude's strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper.
AB - Rewriting logic is both a flexible semantic framework within which widely different concurrent systems can be naturally specified and a logical framework in which widely different logics can be specified. Maude programs are exactly rewrite theories. Maude has also a formal environment of verification tools. Symbolic computation is a powerful technique for reasoning about the correctness of concurrent systems and for increasing the power of formal tools. We present several new symbolic features of Maude that enhance formal reasoning about Maude programs and the effectiveness of formal tools. They include: (i) very general unification modulo user-definable equational theories, and (ii) symbolic reachability analysis of concurrent systems using narrowing. The paper does not focus just on symbolic features: it also describes several other new Maude features, including: (iii) Maude's strategy language for controlling rewriting, and (iv) external objects that allow flexible interaction of Maude object-based concurrent systems with the external world. In particular, meta-interpreters are external objects encapsulating Maude interpreters that can interact with many other objects. To make the paper self-contained and give a reasonably complete language overview, we also review the basic Maude features for equational rewriting and rewriting with rules, Maude programming of concurrent object systems, and reflection. Furthermore, we include many examples illustrating all the Maude notions and features described in the paper.
KW - External objects
KW - Maude and rewriting logic
KW - Meta-interpreters
KW - Strategies
KW - Symbolic model checking
KW - Unification and narrowing
UR - http://www.scopus.com/inward/record.url?scp=85082024320&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85082024320&partnerID=8YFLogxK
U2 - 10.1016/j.jlamp.2019.100497
DO - 10.1016/j.jlamp.2019.100497
M3 - Article
AN - SCOPUS:85082024320
VL - 110
JO - Journal of Logical and Algebraic Methods in Programming
JF - Journal of Logical and Algebraic Methods in Programming
SN - 2352-2208
M1 - 100497
ER -