Symbolic Analysis of Maude Theories with Narval

• Published in: Theory and Practice of Logic Programming
• Main Authors: Alpuente Frasnedo, María, Escobar Román, Santiago, Sapiña-Sanchis, Julia, Ballis, Demis
• Other Authors: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació, Generalitat Valenciana, Agencia Estatal de Investigación, Air Force Office of Scientific Research
• Format: Article in Journal/Newspaper
• Language: English
• Published: Cambridge University Press 2019
• Subjects: Symbolic reachability analysis; Narrowing; Equational unification; Maude; Rewriting logic; LENGUAJES Y SISTEMAS INFORMATICOS; Escobar; Román; narval
• Online Access: http://hdl.handle.net/10251/140495; https://doi.org/10.1017/S1471068419000243

[EN] Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude's symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations. This work has been partially supported by the EU (FEDER) and the Spanish MCIU under grant RTI2018-094403-B-C32, by the Spanish Generalitat Valenciana under grants PROMETEO/2019/098 and APOSTD/2019/127, and by the US Air Force Office of Scientific Research under award number FA9550-17-1-0286. Alpuente Frasnedo, M.; Escobar Román, S.; Sapiña-Sanchis, J.; Ballis, D. (2019). Symbolic Analysis of Maude Theories with Narval. Theory and Practice of Logic Programming. 19(5-6):874-890. https://doi.org/10.1017/S1471068419000243 S 874 890 19 5-6