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.
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.
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.
A ''natural rewriting and narrowing'' prototype interpreter which
improves (weakly) outermost-needed rewriting
and (weakly) outermost-needed narrowing
for non-inductively sequential CSs.
"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.
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 (Graphical VErification and Rewriting for Debugger Internet sistes - Repairing) implements a novel
methodology for semi-automatically repairing faulty Web sites.
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.
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
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.
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.
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.
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).
Software
The following Software has been developed by the ELP group:
A Model Checker for Web applications in Rewriting Logic.
Julienne: a Trace Slicer for Conditional Rewrite Theories
A datalog solver based on Rewriting Logic.
A Fold/Unfold Transformation Framework for Maude Programs.
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.
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.
An automatic prover of narrowing termination.
A static program analyzer based on transforming Datalog query evaluation into parameterised boolean equation system resolution.
A Partial Evaluator for Functional Logic Programs
Here you can find some utilities which can help INDY users to run specialized programs:
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.
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.
An abstract diagnosis based debugger for functional programs.
A ''natural rewriting and narrowing'' prototype interpreter which improves (weakly) outermost-needed rewriting and (weakly) outermost-needed narrowing for non-inductively sequential CSs.
"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.
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 (Graphical VErification and Rewriting for Debugger Internet sistes - Repairing) implements a novel methodology for semi-automatically repairing faulty Web sites.
A machine learning algorithm for inferring distance-based decision trees.
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.
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
A Transformation System for Functional Logic Programs Based on Needed Narrowing. A graphic interface for SYNTH is available here
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.
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.
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.
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).
A compiler for FlatCurry programs into C++ based on memoization.