Trabajos ya publicados

URI permanente para esta colección:

https://hdl.handle.net/11705/2288

Artículos en la categoría Trabajos ya publicados publicados en las Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016).

Examinar

Mostrando 1 - 8 de 8

Abstract analysis of universal properties for tccp
Comini, Marco; Gallardo, María del Mar; Titolo, Laura; Villanueva, Alicia. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
The Timed Concurrent Constraint Language (tccp) is a time extension of the concurrent constraint paradigm of Saraswat. tccp was defined to model reactive systems, where infinite behaviors arise naturally. It is well-known that modeling and analyzing concurrent systems by hand can be an extremely hard task. Thus, the development of automatic formal methods is essential. The particular characteristics of ccp languages make such task even harder, since we have to deal with technical issues due to the infinite computations (natural to reactive systems), use of negative information (particular for ccp languages) and non-determinism. One well established technique to develop semantic-based program analysis is abstract interpretation, which relies on the definition of a specific approximated abstract semantics that captures the information needed to perform the analysis. Typically, one defines an over-approximation of the concrete semantics that includes all possible traces of the system, possibly introducing inexistent ones. This allows one to develop (correct) analysis of universal properties. It does not allow to analyze existential properties, for instance to verify that there exists a suspension trace. This paper (originally published in [1]) defines a framework of over-approximated abstract semantics parametric w.r.t. an abstract constraint system. Since we need to preserve the notion of time—to be able to express properties of interest like safety or time-depending properties—the abstract semantics domains are not Noetherian (even if we use finite abstract constraint systems). Thus, in order to have an effective approach we use a widening to ensure finiteness of the analysis. The abstract semantics is correct and can be represented as a finite graph where each node represents a hypothetical computational step of the program containing approximated information for the variables.
Combining Runtime Checking and Slicing to improve Maude Error Diagnosis
Alpuente, María; Frechina, Francisco; Sapiña, Julia; Ballis, Demis. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
This paper introduces the idea of using assertion checking for enhancing the dynamic slicing of Maude computation traces. Since trace slicing can greatly simplify the size and complexity of the analyzed traces, our methodology can be useful for improving the diagnosis of erroneous Maude programs. The proposed methodology is based on (i) a logical notation for specifying two types of user-defined assertions that are imposed on execution runs: functional assertions and system assertions; (ii) a runtime checking technique that dynamically tests the assertions and is provably safe in the sense that all errors flagged are definite violations of the specifications; and (iii) a mechanism based on equational least general generalization that automatically derives accurate criteria for slicing from falsified assertions.
Reversible Term Rewriting
Nishida, Naoki; Palacios, Adrián; Vidal, Germán. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
Essentially, in a reversible programming language, for each forward computation step from state S to state S', there exists a constructive and deterministic method to go backwards from state S' to state S. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few. In this paper, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step t1 → t2 , we do not always have a decidable and deterministic method to get t1 from t2 . Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define a transformation to make a rewrite system reversible using standard term rewriting. This paper has been published in Naoki Nishida, Adrián Palacios, Germán Vidal. Reversible Term Rewriting. In Delia Kesner and Brigitte Pientka, editors, Proceedings of the First International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. LIPIcs 52, 28:1–28:18, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
River basin management with SPIN
Gallardo, María del Mar; Merino, Pedro; Panizo, Laura; Salmerón, Alberto. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
This paper presents the use of the SPIN model checker as the core engine to build Decision Support Systems (DSSs) to control complex river basins during flood situations. Current DSSs in this domain are mostly based on simulators to predict the rainfall and the water flow along the river basin. In this paper, we propose a scheme that integrates simulators in the water domain with additional logic in P ROMELA to represent basin elements, such as dams, their management rules, the evolution of dam parameters (e.g. level or discharge capacity), and user defined constraints in the whole basin over time. Then, we use the exploration capabilities of SPIN to find out which sequences of operations over the dams produce a global behaviour that mitigates the effect of floods according to user defined constraints along the river basin. Although the method is general for any river basin with dams, it has been evaluated in a real basin in the south of Spain.
Proving termination properties of conditional rewrite systems
Lucas, Salvador; Meseguer, José. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
Conditional Term Rewriting Systems (CTRSs) extend Term Rewriting Systems (TRSs) conditional part c to each rewrite rule l → r, thus obtaining a conditional rewrite rule l → r ⇐ c. The addition of such conditional parts c substantially increases the expressiveness of programming languages that use them and often clarifies the purpose of the rules to make programs more readable and self-explanatory. Computations with CTRSs are defined by means of an Inference System where each rewriting step s →R t requires a proof. This proof-theoretical definition of the operational semantics suggests a natural definition of the termination behavior of R as the absence of infinite proof trees. The notion of operational termination captures this idea, meaning that, given an initial goal, an interpreter will either succeed in finite time in producing a closed proof tree, or will fail in finite time, not being able to close or extend further any of the possible proof trees, after exhaustively searching all such proof trees. Besides implying termination in the usual ‘horizontal’ sense (i.e., as the absence of infinite sequences of rewrite steps), operational termination also captures a ‘vertical’ dimension of the termination behavior which is missing in the usual “without infinite reduction sequences” definition of termination. In [1] we define the notion of V-termination, which captures such a vertical dimension of the termination behavior of CTRSs. We provide a uniform definition of termination and V-termination of CTRSs as the absence of specific kinds of infinite proof trees. We prove that operational termination is just the conjunction of termination and V-termination. We use these results to develop a methodology to prove or disprove termination, V-termination, and operational termination of CTRSs by extending the Dependency Pair (DP) approach for TRSs and generalize the DP approach to all aforementioned termination properties of CTRSs.
Automatic Grading of Programming Exercises using Property-Based Testing
Benac Earle, Clara; Fredlund, Lars-Ake; Hughes, John. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
We present a framework for automatic grading of programming exercises using property-based testing, a form of model-based black-box testing. Models are developed to assess both the functional behaviour of programs and their algorithmic complexity. From the functional correctness model a large number of test cases are derived automatically. Executing them on the body of exercises gives rise to a (partial) ranking of programs, so that a program A is ranked higher than program B if it fails a strict subset of the test cases failed by B. The model for algorithmic complexity is used to compute worst-case complexity bounds. The framework moreover considers code structural metrics, such as McCabe’s cyclomatic complexity, giving rise to a composite program grade that includes both functional, non-functional, and code structural aspects. The framework is evaluated in a course teaching algorithms and data structures using Java.
Polymorphic Types in Erlang Function Specifications
López-Fraguas, Francisco Javier; Montenegro, Manuel; Rodríguez-Hortalá, Juan. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
Erlang is a concurrent functional programming language developed by Ericsson, well suited for implementing distributed systems. Although Erlang is dynamically typed, the Dialyzer static analysis tool can be used to extract implicit type information from the programs, both for documentation purposes and for finding errors that will definitively arise at program execution. Dialyzer is based on the notion of success types, that correspond to safe over-approximations for the semantics of expressions. Erlang also supports user given function specifications (or just specs), that are contracts providing more information about the semantics of functions. Function specs are useful not only as documentation, but also can be employed by Dialyzer to improve the precision of the analysis. Even though specs can have a polymorphic shape, in practice Dialyzer is not able to exploit all their potential. One reason for that is that extending the notion of success type to a polymorphic setting is not trivial, and several interpretations are possible. In this work [1] we propose a precise formulation for a novel interpretation of function specs as polymorphic success types, and a program transformation that allows us to apply this new interpretation on the call sites of functions with a declared spec. This results on a significant improvement in the number of definite errors that Dialyzer is able to detect.
Que Ningún Término Resoluble de Lambda-Valor Se Quede Atrás
García Pérez, Álvaro; Nogueira, Pablo. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
Este es el resumen de la ponencia en Castellano sobre el artículo titulado "No solvable lambda-value term left behind" publicado por los autores en la revista Logical Methods in Computer Science Vol. 2(2:12) 2016, págs.1–43. La ponencia forma parte del programa de las XVI Jornadas sobre Programación y Lenguajes dentro del V Congreso Español de Informática que tuvo lugar del 13 al 16 de septiembre de 2016 en Salamanca.

Examinar

Examinando Trabajos ya publicados por Fecha de publicación

Resultados por página

Opciones de ordenación