Excellence Group PROMETEO/2011/052, PROMETEO-II/2015/013 and PROMETEO/2019/098


The following Software has been developed by the ELP group:


    Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis

  • AGESnew

    Automatic GEneration of order-sorted first-order logical modelS

  • AbsSpec

    A tool for the inference of specifications for Curry programs

  • ACUOS^2new

    Order-Sorted Modular ACU Generalization

  • AirVLC

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

  • Anima

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


    A Tool for enforcing safety assertions in Maude via Program Transformation

  • Datalaude

    A datalog solver based on Rewriting Logic


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


    A graphical tool for exploring (variant) narrowing computations in Maude

  • HEMSnew

    Order-sorted Equational Homeomorphic Embedding Checker

  • iJulienne Online Trace Analyzer

    Slicing-based Trace Analysis of Rewriting Logic Specifications with iJulienne

  • KindSpec new

    A Rewriting-based, Symbolic Abstract Contract Syntheser

  • Learning Systems and other software: Coverage Graphs, gErl, IRT, RROC, Reg2Class, ...new

  • Mau-Dev new

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

  • 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.

  • META - Maudest

    A Fold/Unfold Transformation Framework for Maude Programs.


    Verify termination properties automatically

  • NarradaR

    An automatic prover of narrowing termination

  • NARVALnew

    A Narrowing-based Visual Tool for the Symbolic Analysis of Maude Rewrite Theories,

  • PRESTOnew

    Program Rule-and-Equation Specializer for Maude TheOries

  • Victoria

    A Partial Evaluator for Maude

  • Web-TLR

    A Model Checker for Web applications in Rewriting Logic

  • WifiX: verification and repairing tool of XML repositories

    Rewriting-based Repairing Strategies for XML Documents

  • Other tools for the reflective programming language Maude
    • Automatic Certification of Java Source Code in Rewriting Logic
    • Evaluation with on-demand strategy annotations
    • New and redefinition of Maude commands
    • 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 maude.cs.uiuc.edu/download and the latest version is always available at www.lcc.uma.es/~duran/FullMaude.

  • Other Tools
    • An Automatic Useless Argument Elimination System

    • BUGGY

      A declarative debugger for functional logic programs.

    • DBDT

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

    • Debussy

      An abstract diagnosis based debugger for functional programs.

    • FLIP v0.7

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

    • GVerdi-R

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

    • 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.
    • Natur

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

    • SMILES

      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.

    • 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.

  • Semantics-Based Tools for the Multi-Paradigm Language Curry
    • 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).

    • 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.

    • 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

    • 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.

    • SYNTH

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

    • Tabasco

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

    • 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.