Germán Vidal

LOPSTR Conference 2021 Conference Paper

Prefix-Based Tracing in Message-Passing Concurrency

• Juan José González-Abril
• Germán Vidal

Abstract The execution of concurrent applications typically involves some degree of nondeterminism, mostly due to the relative speeds of concurrent processes. An essential task in state-space exploration techniques for the verification of concurrent programs consists in finding points in an execution where alternative actions are possible. Here, the nondeterministic executions of a program can be represented by a tree-like structure. Given the trace of a concrete execution, one first identifies its branching points. Then, a new execution can be steered up to one of these branching points (using, e. g. , a partial trace), so that an unexplored branch can be considered. From this point on, the execution proceeds nondeterministically, eventually producing a trace of the complete execution as a side-effect, and the process starts again. In this paper, we formalize this operation—partially driving the execution of a program and then producing a trace of the entire execution—, which we call prefix-based tracing. It combines ideas from both record-and-replay debugging and execution tracing. We introduce a semantics-based formalization of prefix-based tracing in the context of a message-passing concurrent language like Erlang. Furthermore, we also present an implementation of prefix-based tracing by means of a program instrumentation.

LOPSTR Conference 2016 Conference Paper

A Reversible Semantics for Erlang

• Naoki Nishida 0001
• Adrián Palacios
• Germán Vidal

Abstract In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for debugging and for enforcing fault-tolerance, among others. In this paper, we consider a subset of Erlang, a concurrent language based on the actor model, and formally introduce a semantics for reversible computation. To the best of our knowledge, this is the first attempt to define a reversible semantics for Erlang.

LOPSTR Conference 2016 Conference Paper

On the Completeness of Selective Unification in Concolic Testing of Logic Programs

• Fred Mesnard
• Étienne Payet
• Germán Vidal

Abstract Concolic testing is a popular dynamic validation technique that can be used for both model checking and automatic test case generation. We have recently introduced concolic testing in the context of logic programming. In contrast to previous approaches, the key ingredient in this setting is a technique to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. This is called “selective” unification. In this paper, we show that the existing algorithm is not complete and explore different alternatives in order to have a sound and complete algorithm for selective unification.

LOPSTR Conference 2016 Conference Paper

Symbolic Execution and Thresholding for Efficiently Tuning Fuzzy Logic Programs

• Ginés Moreno
• Jaime Penabad
• José A. Riaza
• Germán Vidal

Abstract Fuzzy logic programming is a growing declarative paradigm aiming to integrate fuzzy logic into logic programming. One of the most difficult tasks when specifying a fuzzy logic program is determining the right weights for each rule, as well as the most appropriate fuzzy connectives and operators. In this paper, we introduce a symbolic extension of fuzzy logic programs in which some of these parameters can be left unknown, so that the user can easily see the impact of their possible values. Furthermore, given a number of test cases, the most appropriate values for these parameters can be automatically computed. Finally, we show some benchmarks that illustrate the usefulness of our approach.

LOPSTR Conference 2015 Conference Paper

Concolic Execution in Functional Programming by Program Instrumentation

• Adrián Palacios
• Germán Vidal

Abstract Concolic execution, a combination of concrete and symbolic execution, has become increasingly popular in recent approaches to model checking and test case generation. In general, an interpreter of the language is augmented in order to also deal with symbolic values. In this paper, in contrast, we present an alternative approach that is based on a program instrumentation. Basically, the execution of the instrumented program in a standard environment produces a sequence of events that can be used to reconstruct the associated symbolic execution.

LOPSTR Conference 2014 Conference Paper

Concolic Execution and Test Case Generation in Prolog

• Germán Vidal

Abstract Symbolic execution extends concrete execution by allowing symbolic input data and then exploring all feasible execution paths. It has been defined and used in the context of many different programming languages and paradigms. A symbolic execution engine is at the heart of many program analysis and transformation techniques, like partial evaluation, test case generation or model checking, to name a few. Despite its relevance, traditional symbolic execution also suffers from several drawbacks. For instance, the search space is usually huge (often infinite) even for the simplest programs. Also, symbolic execution generally computes an overapproximation of the concrete execution space, so that false positives may occur. In this paper, we propose the use of a variant of symbolic execution, called concolic execution, for test case generation in Prolog. Our technique aims at full statement coverage. We argue that this technique computes an underapproximation of the concrete execution space (thus avoiding false positives) and scales up better to medium and large Prolog applications.

I&C Journal 2014 Journal Article

Fast offline partial evaluation of logic programs

• Michael Leuschel
• Germán Vidal

One of the most important challenges in partial evaluation is the design of automatic methods for ensuring the termination of the process. In this work, we introduce sufficient conditions for the strong (i. e. , independent of a computation rule) termination and quasi-termination of logic programs which rely on the construction of size-change graphs. We then present a fast binding-time analysis that takes the output of the termination analysis and annotates logic programs so that partial evaluation terminates. In contrast to previous approaches, the new binding-time analysis is conceptually simpler and considerably faster, scaling to medium-sized or even large examples.

LOPSTR Conference 2013 Conference Paper

A Finite Representation of the Narrowing Space

• Naoki Nishida 0001
• Germán Vidal

Abstract Narrowing basically extends rewriting by allowing free variables in terms and by replacing matching with unification. As a consequence, the search space of narrowing becomes usually infinite, as in logic programming. In this paper, we introduce the use of some operators that allow one to always produce a finite data structure that still represents all the narrowing derivations. Furthermore, we extract from this data structure a novel, compact equational representation of the (possibly infinite) answers computed by narrowing for a given initial term. Both the finite data structure and the equational representation of the computed answers might be useful in a number of areas, like program comprehension, static analysis, program transformation, etc.

LOPSTR Conference 2013 Conference Paper

Towards Erlang Verification by Term Rewriting

• Germán Vidal

Abstract This paper presents a transformational approach to the verification of Erlang programs. We define a stepwise transformation from (first-order) Erlang programs to (non-deterministic) term rewrite systems that compute an overapproximation of the original Erlang program. In this way, existing techniques for term rewriting become available. Furthermore, one can use narrowing as a symbolic execution extension of rewriting in order to design a verification technique. We illustrate our approach with some examples, including a deadlock analysis of a simple Erlang program.

LOPSTR Conference 2012 Conference Paper

Computing More Specific Versions of Conditional Rewriting Systems

• Naoki Nishida 0001
• Germán Vidal

Abstract Rewrite systems obtained by some automated transformation often have a poor syntactic structure even if they have good properties from a semantic point of view. For instance, a rewrite system might have overlapping left-hand sides even if it can only produce at most one constructor normal form (i. e. , value). In this paper, we propose a method for computing “more specific” versions of deterministic conditional rewrite systems (i. e. , typical functional programs) by replacing a given rule (e. g. , an overlapping rule) with a finite set of instances of this rule. In some cases, the technique is able to produce a non-overlapping system from an overlapping one. We have applied the transformation to improve the systems produced by a previous technique for function inversion with encouraging results (all the overlapping systems were successfully transformed to non-overlapping systems).

TCS Journal 2012 Journal Article

Preface

• Matthias Blume
• Germán Vidal

LOPSTR Conference 2010 Conference Paper

A Hybrid Approach to Conjunctive Partial Evaluation of Logic Programs

• Germán Vidal

Abstract Conjunctive partial deduction is a well-known technique for the partial evaluation of logic programs. The original formulation follows the so called online approach where all termination decisions are taken on-the-fly. In contrast, offline partial evaluators first analyze the source program and produce an annotated version so that the partial evaluation phase should only follow these annotations to ensure the termination of the process. In this work, we introduce a lightweight approach to conjunctive partial deduction that combines some of the advantages of both online and offline styles of partial evaluation.

LOPSTR Conference 2009 Conference Paper

Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing

• José Iborra
• Naoki Nishida 0001
• Germán Vidal

Abstract In this work, we first consider a goal-oriented extension of the dependency pair framework for proving termination w. r. t. a given set of initial terms. Then, we introduce a new result for proving relative termination in terms of a dependency pair problem. Both contributions put together allow us to define a simple and powerful approach to analyzing the termination of narrowing, an extension of rewriting that replaces matching with unification in order to deal with logic variables. Our approach could also be useful in other contexts where considering termination w. r. t. a given set of terms is also natural (e. g. , proving the termination of functional programs).

LOPSTR Conference 2009 Conference Paper

Towards Scalable Partial Evaluation of Declarative Programs

• Germán Vidal

Abstract Partial evaluation is a well-known technique for program specialization [4]. Essentially, given a program and part of its input data—the so-called static data—a partial evaluator returns a new, residual program which is specialized for the given data. The residual program is then used for performing the remaining computations—those that depend on the so-called dynamic data.

LOPSTR Conference 2008 Conference Paper

A Transformational Approach to Polyvariant BTA of Higher-Order Functional Programs

• Gustavo Arroyo
• J. Guadalupe Ramos
• Salvador Tamarit
• Germán Vidal

Abstract We introduce a transformational approach to improve the first stage of offline partial evaluation of functional programs, the so called binding-time analysis (BTA). For this purpose, we first introduce an improved defunctionalization algorithm that transforms higher-order functions into first-order ones, so that existing techniques for termination analysis and propagation of binding-times of first-order programs can be applied. Then, we define another transformation (tailored to defunctionalized programs) that allows us to get the accuracy of a polyvariant BTA from a monovariant BTA over the transformed program. Finally, we show a summary of experimental results that demonstrate the usefulness of our approach.

LOPSTR Conference 2008 Conference Paper

Fast Offline Partial Evaluation of Large Logic Programs

• Michael Leuschel
• Germán Vidal

Abstract In this paper, we present a fast binding-time analysis (BTA) by integrating a size-change analysis, which is independent of a selection rule, into a classical BTA for offline partial evaluation of logic programs. In contrast to previous approaches, the new BTA is conceptually simpler and considerably faster, scaling to medium-sized or even large examples and, moreover, it ensures both the so called local and global termination. We also show that through the use of selective hints, we can achieve both good specialisation results and a fast BTA and specialisation process.

LOPSTR Conference 2007 Conference Paper

Preserving Sharing in the Partial Evaluation of Lazy Functional Programs

• Sebastian Fischer 0001
• Josep Silva
• Salvador Tamarit
• Germán Vidal

Abstract The goal of partial evaluation is the specialization of programs w. r. t. part of their input data. Although this technique is already well-known in the context of functional languages, current approaches are either overly restrictive or destroy sharing through the specialization process, which is unacceptable from a performance point of view. In this work, we present the basis of a new partial evaluation scheme for first-order lazy functional programs that preserves sharing through the specialization process and still allows the unfolding of arbitrary function calls.

JELIA Conference 2006 Conference Paper

A Slicing Tool for Lazy Functional Logic Programs

• Claudio Ochoa
• Josep Silva
• Germán Vidal

Abstract Program slicing is a well-known technique that has been widely used for debugging in the context of imperative programming. Debugging is a particularly difficult task within lazy declarative programming. In particular, there exist very few approaches to program slicing in this context. In this paper, we describe a slicing tool for first-order lazy functional logic languages. We also illustrate its usefulness by means of an example.

LOPSTR Conference 2006 Conference Paper

Improving Offline Narrowing-Driven Partial Evaluation Using Size-Change Graphs

• Gustavo Arroyo
• J. Guadalupe Ramos
• Josep Silva
• Germán Vidal

Abstract An offline approach to narrowing-driven partial evaluation (a partial evaluation scheme for first-order functional and functional logic programs) has recently been introduced. In this approach, program annotations (i. e. , the expressions that should be generalised at partial evaluation time to ensure termination) are based on a simple syntactic characterisation of quasi-terminating programs. This work extends the previous offline scheme by introducing a new annotation strategy which is based on a combination of size-change graphs and binding-time analysis. Preliminary experiments point out that the number of program annotations is significantly reduced compared to the previous approach, which means that faster residual programs are often produced.

TCS Journal 2004 Journal Article

Rules + strategies for transforming lazy functional logic programs

• Marı́a Alpuente
• Moreno Falaschi
• Ginés Moreno
• Germán Vidal

This work introduces a transformation methodology for functional logic programs based on needed narrowing, the optimal and complete operational principle for modern declarative languages which integrate the best features of functional and logic programming. We provide correctness results for the transformation system w. r. t. the set of computed values and answer substitutions and show that the prominent properties of needed narrowing—namely, the optimality w. r. t. the length of derivations and the number of computed solutions—carry over to the transformation process and the transformed programs. We illustrate the power of the system by taking on in our setting two well-known transformation strategies (composition and tupling). We also provide an implementation of the transformation system which, by means of some experimental results, highlights the potentiality of our approach.

LOPSTR Conference 2004 Conference Paper

Run-Time Profiling of Functional Logic Programs

• Bernd Braßel
• Michael Hanus
• Frank Huch
• Josep Silva
• Germán Vidal

Abstract In this work, we introduce a profiling scheme for modern functional logic languages covering notions like laziness, sharing, and non-determinism. Firstly, we instrument a natural (big-step) semantics in order to associate a symbolic cost to each basic operation (e. g. , variable updates, function unfoldings, case evaluations). While this cost semantics provides a formal basis to analyze the cost of a computation, the implementation of a cost-augmented interpreter based on it would introduce a huge overhead. Therefore, we also introduce a sound transformation that instruments a program such that its execution—under the standard semantics—yields not only the corresponding results but also the associated costs. Finally, we describe a prototype implementation of a profiler based on the developments in this paper.

LOPSTR Conference 2002 Conference Paper

Forward Slicing of Multi-paradigm Declarative Programs Based on Partial Evaluation

• Germán Vidal

Abstract Program slicing has been mainly studied in the context of imperative languages, where it has been applied to many software engineering tasks, like program understanding, maintenance, debugging, testing, code reuse, etc. This paper introduces the first forward slicing technique for multi-paradigm declarative programs. In particular, we show how program slicing can be defined in terms of online partial evaluation. Our approach clarifies the relation between both methodologies and provides a simple way to develop program slicing tools from existing partial evaluators.

LOPSTR Conference 2001 Conference Paper

Symbolic Profiling for Multi-paradigm Declarative Languages

• Elvira Albert
• Germán Vidal

Abstract We present the basis of a source-level profiler for multi-paradigm declarative languages which integrate features from (lazy) functional and logic programming. Our profiling scheme is symbolic in the sense that it is independent of the particular language implementation. This is achieved by counting the number of basic operations performed during the execution of program calls, e. g. , the number of unfolding steps, the number of matching operations, etc. The main contribution of this paper is the formal specification of the attribution of execution costs to cost centers, which is particularly difficult in the context of lazy languages. A prototype implementation of the symbolic profiler has been undertaken for the multi-paradigm language Curry. Preliminary results demonstrate the practicality of our approach and its applications in the field of program transformation.

LOPSTR Conference 2000 Conference Paper

Measuring the Effectiveness of Partial Evaluation

• Elvira Albert
• Sergio Antoy
• Germán Vidal

LPAR Conference 2000 Conference Paper

Using an Abstract Representation to Specialize Functional Logic Programs

• Elvira Albert
• Michael Hanus
• Germán Vidal

Abstract This paper introduces a novel approach for the specialization of functional logic languages. We consider a maximally simplified abstract representation of programs (which still contains all the necessary information) and define a non-standard semantics for these programs. Both things mixed together allow us to design a simple and concise partial evaluation method for modern functional logic languages, avoiding several limitations of previous approaches. Moreover, since these languages can be automatically translated into the abstract representation, our technique is widely applicable. In order to assess the practicality of our approach, we have developed a partial evaluation tool for the multi-paradigm language Curry. The partial evaluator is written in Curry itself and has been tested on an extensive benchmark suite (even a meta-interpreter). To the best of our knowledge, this is the first purely declarative partial evaluator for a functional logic language.

LPAR Conference 1999 Conference Paper

A Partial Evaluation Framework for Curry Programs

• Elvira Albert
• María Alpuente
• Michael Hanus
• Germán Vidal

Abstract In this work, we develop a partial evaluation technique for residuating functional logic programs, which generalize the concurrent computation models for logic programs with delays to functional logic programs. We show how to lift the nondeterministic choices from run time to specialization time. We ascertain the conditions under which the original and the transformed program have the same answer expressions for the considered class of queries as well as the same floundering behavior. All these results are relevant for program optimization in Curry, a functional logic language which is intended to become a standard in this area. Preliminary empirical evaluation of the specialized Curry programs demonstrates that our technique also works well in practice and leads to substantial performance improvements. To our knowledge, this work is the first attempt to formally define and prove correct a general scheme for the partial evaluation of functional logic programs with delays.

TCS Journal 1996 Journal Article

A compositional semantic basis for the analysis of equational Horn programs

• María Alpuente
• Moreno Falaschi
• Germán Vidal

We introduce a compositional characterization of the operational semantics of equational Horn programs. Then we show that this semantics and the standard operational semantics based on (basic) narrowing coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient AND-compositional program analysis. As an application of our framework, we show a compositional analysis to detect the unsatisfiability of an equation set with respect to a given equational theory. We also show that our method allows us to perform computations and analysis incrementally in a Constraint Equational setting and that the test of satisfiability in this setting can be done in parallel.