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.
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.
GVerdi-R (Graphical VErification and Rewriting for Debugger Internet sistes - Repairing) implements a novel
methodology for semi-automatically repairing faulty Web sites.
A ''natural rewriting and narrowing'' prototype interpreter which
improves (weakly) outermost-needed rewriting
and (weakly) outermost-needed narrowing
for non-inductively sequential CSs.
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.
"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.
Semantics-Based Tools for the Multi-Paradigm Language Curry
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).
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.
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.
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.
Software
The following Software has been developed by the ELP group:
Safety enforcement via programmable strategies in Maude
Combining Runtime Checking and Slicing to Improve Maude Error Diagnosis
Automatic GEneration of order-sorted first-order logical modelS
A tool for the inference of specifications for Curry programs
Order-Sorted Modular ACU Generalization
Real-time urban air pollution forecasts using machine learning for the city of Valencia in Spain
Inspecting Rewriting Logic Computations (in a parametric and stepwise way)
A Tool for enforcing safety assertions in Maude via Program Transformation
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
Order-sorted Equational Homeomorphic Embedding Checker
Slicing-based Trace Analysis of Rewriting Logic Specifications with iJulienne
incremental Program Rule-and-Equation Specializer for Maude TheOries
A Partial Evaluator for Maude
A Rewriting-based, Symbolic Abstract Contract Syntheser
A developer extension of Maude 2.7 that includes some efficient developer (meta-level) operations
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 Fold/Unfold Transformation Framework for Maude Programs.
Verify termination properties automatically
An automatic prover of narrowing termination
A Narrowing-based Visual Tool for the Symbolic Analysis of Maude Rewrite Theories,
Program Rule-and-Equation Specializer for Maude TheOries
A Partial Evaluator for Maude
A Model Checker for Web applications in Rewriting Logic
Rewriting-based Repairing Strategies for XML Documents
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.
A declarative debugger for functional logic programs.
A machine learning algorithm for inferring distance-based decision trees.
An abstract diagnosis based debugger for functional programs.
The FLIP system is an application that implements a framework for the Induction of Functional Logic Programs (IFLP).
GVerdi-R (Graphical VErification and Rewriting for Debugger Internet sistes - Repairing) implements a novel methodology for semi-automatically repairing faulty Web sites.
A Partial Evaluator for Functional Logic Programs
Here you can find some utilities which can help INDY users to run specialized programs:
A ''natural rewriting and narrowing'' prototype interpreter which improves (weakly) outermost-needed rewriting and (weakly) outermost-needed narrowing for non-inductively sequential CSs.
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.
"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.
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).
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.
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.
A Transformation System for Functional Logic Programs Based on Needed Narrowing. A graphic interface for SYNTH is available here
A compiler for FlatCurry programs into C++ based on memoization.
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.