Navegación

Búsqueda

Búsqueda avanzada

El autor Enrique Martin-Martin ha publicado 3 artículo(s):

1 - A liberal type system for functional logic programs

We propose a new type system for functional logic programming which is more liberal than the classical DamasMilner usually adopted, but it is also restrictive enough to ensure type soundness. Starting from DamasMilner typing of expressions, we propose a new notion of well-typed program that adds support for type-indexed functions, a particular form of existential types, opaque higherorder patterns and generic functions as shown by an extensive collection of examples that illustrate the possibilities of our proposal. In the negative side, the types of functions must be declared, and therefore types are checked but not inferred. Another consequence is that parametricity is lost, although the impact of this flaw is limited as free theorems were already compromised in functional logic programming because of non-determinism.

Autores: Francisco J. López-Fraguas / Enrique Martin-Martin / Juan Rodríguez-Hortalá / 
Palabras Clave:

2 - EDD: A Declarative Debugger for Sequential Erlang Programs (High-level Work)

Declarative debuggers are semi-automatic debugging tools that abstract the execution details to focuson the program semantics. This paper presents a tool implementing this approach for the sequentialsubset of Erlang, a functional language with dynamic typing and strict evaluation. Given an erro-neous computation, it first detects an erroneous function (either a «named» function or a lambda-abstraction), and then continues the process to identify the fragment of the function responsible forthe error. Among its features it includes support for exceptions, predefined and built-in functions,higher-order functions, and trusting and undo commands.

Autores: Rafael Caballero / Enrique Martin-Martin / Adrián Riesco / 
Palabras Clave:

3 - Verification of ROS Navigation using Maude

The Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The emph{Navigation Stack} stands out among the different libraries available in ROS. This library provides a set of reusable components that developers can use to build robots with autonomous navigation capabilities. This is a critical component, as navigation failures could have catastrophical consequences for applications like self-driving cars.Here we show our work on the verification of the C++ code for the navfn planner, which is the main planner component of the Navigation Stack. We have ported the planner to a Maude specification, and validated their equivalence using differential testing techniques. For this purpose, we integrated the specification into ROS using a novel high performance Python interface for Maude. We then analyzed the Maude specification by means of model checking and functional verification techniques, using not only the built-in tools of Maude, but also a translation into Dafny, and a manual but systematic generation of verification conditions from the Maude specification. Along the way we also encountered counterexamples for some soundness properties —e.g. that paths should not collide with obstacles— and optimatility —paths should have the lowest possible cost— of the NavFn planner.

Autores: Enrique Martin-Martin / Manuel Montenegro / Adrián Riesco / Juan Rodríguez-Hortalá / Rubén Rubio / 
Palabras Clave: Dafny - Formal Verification - Maude - Model checking - Navigation - Rewriting Logic - ROS