The following Software has been developed by the ELP group:

  • KindSpec2 new

    A Rewriting-based, Symbolic Abstract Contract Syntheser

  • ABETS new

    Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis

  • Mau-Dev new

    A developer extension of Maude 2.7 that includes some efficient developer (meta-level) operations

  • Anima

    Inspecting Rewriting Logic Computations (in a parametric and stepwise way)

  • AirVLCnew

    AIRVLC: Real-time urban air pollution forecasts using machine learning for the city of Valencia in Spain

  • ACUOSnew

    ACUOS: Order-Sorted Modular ACU Generalization

  • iJulienne Online Trace Analyzer

    Slicing-based Trace Analysis of Rewriting Logic Specifications with iJulienne

  • WifiX: verification and repairing tool of XML repositories

    Rewriting-based Repairing Strategies for XML Documents

  • Web-TLR

    A Model Checker for Web applications in Rewriting Logic.

  • AbsSpec

    A tool for the inference of specifications for Curry programs

  • Slicing Tool for RWL

    Julienne: a Trace Slicer for Conditional Rewrite Theories

  • Datalaude

    A datalog solver based on Rewriting Logic.

  • META - Maudest

    A Fold/Unfold Transformation Framework for Maude Programs.

  • Narrowing in Maude

    Narrowing is a generalization of term rewriting that allows free variables in terms (as in logic programming) and replaces pattern matching by unification in order to (non-deterministically) reduce these terms. Narrowing was originally introduced as a mechanism for solving equational unification problems and then generalized to solve the more general problem of symbolic reachability. The narrowing mechanism has a number of important applications including automated proofs of termination, execution of functional-logic programming languages, partial evaluation, verification of cryptographic protocols, symbolic model checking, and equational unification.

    A search command based on narrowing and a narrowing-based unification command for symbols with associativity, commutativity, and identity have been included in Full Maude. Details on their features and syntax, as well as several examples, are available in the Maude Manual.

    Full Maude is available at the Maude site and the latest version is always available at

  • MAUDE-NPAnew

    Maude-NPA is an analysis tool for cryptographic protocols that takes into account many of the algebraic properties of cryptosystems that are not included in other tools. These include cancellation of encryption and decryption, Abelian groups (including exclusive-or), and exponentiation. Maude-NPA uses an approach similar to the original NRL Protocol Analyzer; it is based on unification, and performs backwards search from a final state to determine whether or not it is reachable. Unlike the original NPA, it has a theoretical basis in rewriting logic and narrowing, and offers support for a wider basis of equational theories that includes associative-commutative (AC) theories.

  • Evaluation with on-demand strategy annotationsnew
  • Other tools for the reflective programming language Maude
  • NarradaR

    An automatic prover of narrowing termination.


    A static program analyzer based on transforming Datalog query evaluation into parameterised boolean equation system resolution.

  • INDY v1.8

    A Partial Evaluator for Functional Logic Programs

    Here you can find some utilities which can help INDY users to run specialized programs:

    • indy2curry: a translator from INDY syntax to Curry syntax;
    • curry2indy: a translator from Curry syntax to INDY syntax.
  • FLIP v0.7

    The FLIP system is an application that implements a framework for the Induction of Functional Logic Programs (IFLP).


    A declarative debugger for functional logic programs.

  • An Automatic Useless Argument Elimination System

    A prototype system for the analysis and elimination of redundant arguments in functions.


    A machine learning system that integrates many different features from other machine learning techniques and paradigms and, more importantly, it presents several innovations in many of these features.

  • Debussy

    An abstract diagnosis based debugger for functional programs.

  • Natur

    A ''natural rewriting and narrowing'' prototype interpreter which improves (weakly) outermost-needed rewriting and (weakly) outermost-needed narrowing for non-inductively sequential CSs.

  • Verdi

    "VErification and Rewriting for Debugging Internet Sites", which is a system prototype being able to detect missing as well as incomplete Web pages w.r.t. a given formal specification.

  • Web Verdi

    New rewriting-based Web verification service based on the system Verdi. It is able to detect incorrect/forbidden information as well as incomplete/missing Web pages in a Web site w.r.t a given formal specification.

  • GVerdi-R

    GVerdi-R (Graphical VErification and Rewriting for Debugger Internet sistes - Repairing) implements a novel methodology for semi-automatically repairing faulty Web sites.

  • DBDT

    A machine learning algorithm for inferring distance-based decision trees.

  • Semantics-Based Tools for the Multi-Paradigm Language Curry
    • UPV-Curry

      An Incremental Curry Interpreter with polymorphic types and monadic declarative I/O.

      Here you can find an example Curry program which simulates the ecological behavior of the Segura river's basin. A description of this application (in spanish) can be found here.

    • Partial Evaluator

      This is a purely declarative partial evaluator written in Curry itself. In contrast to INDY, it is able to deal with all the features of a modern functional logic language by translating source programs into the intermediate language FlatCurry

    • SYNTH

      A Transformation System for Functional Logic Programs Based on Needed Narrowing. A graphic interface for SYNTH is available here

    • Source-Level Symbolic Profiler

      Two main features characterize our profiler: Our scheme is defined for the source language; hence, the attribution of costs to the user's program is straightforward. The profiler is "symbolic"; this means that it is independent of a particular implementation of the language. We do not return actual execution times but a list of symbolic measures: the number of computation steps, the number of allocated cells, the number of nondeterministic branches, and the number of pattern matching operations.

    • Cost-Augmented Partial Evaluator

      This is an extension of the partial evaluator above which incorporates the computation of symbolic costs. It also includes a simple speedup analysis which allows us to determine the concrete improvement achieved by the specialization process.

    • Forward Slicing Tool

      By exploting the similarities between (forward) slicing and (online) partial evaluation, we developed a forward slicing tool for Curry. The (forward) slicing tool has been implemented by adapting the partial evaluator above. It required a small implementation effort, i.e., only the underlying meta-interpreter needed significant changes.

    • A List-Processing Optimizer

      The system implements source-to-source transformations for improving the efficiency of list-processing functions in Curry programs. In particular, we consider two list-processing optimizations which are fully automatic: an adaptation of the short cut deforestation (from functional programming) and a technique to introduce accumulating parameters (inspired by the logic programming difference-list transformation).

    • Tabasco

      A compiler for FlatCurry programs into C++ based on memoization.