# Symbolic Analysis of Maude Theories with Narval

## TL;DR

This paper introduces Narval, a graphical tool designed to simplify the programming and analysis of Maude rewrite theories by providing detailed inspection of symbolic computations, enhancing understanding for users.

## Contribution

The paper presents Narval, a novel graphical tool that improves the usability and comprehension of Maude's symbolic reasoning capabilities for complex rewrite theories.

## Key findings

- Narval enables detailed visualization of symbolic Maude computations.
- It facilitates easier debugging and understanding of nondeterministic behaviors.
- The tool supports complex equational reasoning and reachability analysis.

## Abstract

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 paper is under consideration for acceptance in TPLP.