Symbolic Analysis of Maude Theories with Narval

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. Intricate computing problems may be effectively and naturally solved thanks to the synergic mixture of symbolic capabilities with 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) reachability analysis of rewrite theories modulo equational theories. The recent inclusion of symbolic capabilities in Maude is based on narrowing, a generalization of term rewriting that allows logical variables in terms, and provides Maude with logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis, thus increasing the effectiveness of Maude's formal tools. However, the combination of all these features hinders the understanding of Maude symbolic computations for non-experienced developers. The purpose of this system description is to present how programming and analysis of Maude theories can be made easy by providing a graphical tool that supports visualization and animation facilities of Maude narrowing computations.