Jornadas sobre Programación y Lenguajes (PROLE)

URI permantente para esta comunidad:

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

Las Jornadas de PROgramación y LEnguajes (PROLE) constituyen un marco propicio de reunión, debate y divulgación para los grupos españoles que investigan en temas relacionados con la programación y los lenguajes de programación. Con la organización de este evento nacido en 2001, de carácter anual, se pretende fomentar el intercambio de experiencias y resultados, así como la comunicación y cooperación entre dichos grupos.

Examinar

Mostrando 1 - 20 de 191

A characterisation of reliability tools for Software Defined Networks
Lavado, Leticia; Panizo, Laura; Gallardo, María del Mar; Merino, Pedro. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.
Software Defined Network (SDN) is a new paradigm in networking that introduces great flexibility, allowing the dynamic configuration of parts of the network through centralised programming. SDN has been successfully applied in field networks, and is now being applied to wireless and mobile networks, generating Software Defined Mobile/Wireless networks (SDWNs). SDN can be also combined with Network Function Virtualization (NFV) producing a software network in which the specific hardware is replaced by general purpose computing equipment running SDN and NFV software solutions. This highly programmable and flexible network introduces many challenges from the point of view of reliability (or robustness), and operators need to ensure the same level of confidence as in previous, less flexible deployments. This paper provides a first study of the current tools used to analyse the reliability of SDNs before deployment and/or during the exploitation of the network. Most of these tools offer some kind of automatic verification, supported by algorithms based on formal methods, but they do not differentiate between fixed and mobile/wireless networks. In the paper we provide a number of classifications of the tools to make this selection easier for potential users, and we also identify promising research areas where more effort needs to be made.
A characterization of local confluence of conditional term rewriting systems
Lucas, Salvador. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.
When using non-deterministic reduction-based systems, guaranteeing that two diverging steps can be eventually rejoined is crucial for a faithful use in most applications. This property of reduction systems is called local confluence. Gérard Huet provided a characterization of local confluence for term rewriting systems. In conditional term rewriting systems, reduction steps may depend on the satisfaction of specific conditions in rules. Although conditional rewriting was introduced and used already in the 1970s and deeply investigated in the early 1980s, only partial characterizations or sufficient conditions of local confluence of conditional term rewriting have been obtained so far. In this paper, we char- acterize local confluence of conditional rewrite systems as the joinability of a set of conditional pairs including the usual conditional critical pairs and a new kind of pairs we call conditional variable pairs.
A Collection of Website Benchmarks Labelled for Template Detection and Content Extraction
Alarte, Julián; Insa, David; Sílva, Josep; Tamarit, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Template detection and content extraction are two of the main areas of information retrieval applied to the Web. They perform different analyses over the structure and content of webpages to extract some part of the document. However, their objectives are different. While template detection identifies the template of a webpage (usually comparing with other webpages of the same website), content extraction identifies the main content of the webpage discarding the other part. Therefore, they are somehow complementary, because the main content is not part of the template. It has been measured that templates represent between 40% and 50% of data on the Web. Therefore, identifying templates is essential for indexing tasks because templates usually contain irrelevant information such as advertisements, menus and banners. Processing and storing this information is likely to lead to a waste of resources (storage space, bandwidth, etc.). Similarly, identifying the main content is essential for many information retrieval tasks. In this paper, we present a benchmark suite to test different approaches for template detection and content extraction. The suite is public, and it contains real heterogeneous webpages that have been labelled so that different techniques can be suitable (and automatically) compared.
A Correct Compiler from Mini-ML to a Big-Step Machine Verified Using Natural Semantics in Coq
Zúñiga, Ángel; Bel-Enguix, Gemma. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
This paper presents a correct compiler of a small functional language, Mini-ML, formalized in Coq. The literature of functional compiler verification in proof assistants usually reports the use of ad hoc formalizations. This work emphasized the use of natural semantics as uniform and unifying framework for this task. As a result of following this approach, a new big-step semantics machine with call by value is introduced, inspired by the SECD of Landin and the MSECD of Leroy. Since this machine uses de Bruijn indices, as first step is giving a (correct verified) translation from named Mini-ML to de Bruijn notation Mini-ML in the natural semantics setting. To the best of the author's knowledge, this is the first mechanization of a correct compiler of a functional language, using natural semantics as verifying framework in a proof assistant, such as, a working compiler capable to be used in real life can be obtained from it.
A Datalog Framework for Modeling Relationship-based Access Control Policies
Pasarella, Edelmira; Lobo, Jorge. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
Relationships like friendship to limit access to resources have been part of social network applications since their beginnings. Describing access control policies in terms of relationships is not particular to social networks and it arises naturally in many situations. Hence, we have recently seen several proposals formalizing different Relationship-based Access Control (ReBAC) models. In this paper, we introduce a class of Datalog programs suitable for modeling ReBAC and argue that this class of programs, that we called ReBAC Datalog policies, provides a very general framework to specify and implement ReBAC policies. To support our claim, we first formalize the merging of two recent proposals for modeling ReBAC, one based on hybrid logic and the other one based on path regular expressions. We present extensions to handle negative authorizations and temporal policies. We describe mechanism for policy analysis, and then discuss the feasibility of using Datalog-based systems as implementations.
A Declarative Debugger for Concurrent Erlang Programs
Caballero, Rafael; Martin-Martin, Enrique; Riesco, Adrián; Tamarit, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Erlang is a concurrent language with features such as actor model concurrency, no shared memory, message passing communication, high scalability and availability. However, the development of concurrent programs is a complex and error prone task. In this paper we present a declarative debugging approach for concurrent Erlang programs. Our debugger asks questions about the validity of transitions between the different points of the program that involve message passing and/or process creation. The answers, which represent the intended behavior of the program, are compared with the transitions obtained in an actual execution of the program. The differences allow us to detect program errors and to point out the pieces of source code responsible for the bugs. In order to represent the computations we present a semantic calculus for concurrent Core Erlang programs. The debugger uses the proof trees in this calculus as debugging trees used for selecting the questions asked to the user. The relation between the debugging trees and the semantic calculus allows us to establish the soundness of the approach. The theoretical ideas have been implemented in a debugger prototype.
A Declarative Semantics for a Fuzzy Logic Language Managing Similarities and Truth Degrees
Julián Iranzo, Pascual; Moreno, Ginés; Penabad, Jaime; Vázquez, Carlos. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
This work proposes a declarative semantics based on a fuzzy variant of the classical notion of least Herbrand model for the so-called FASILL language (acronym of “Fuzzy Aggregators and Similarity Into a Logic Language”) which has being recently designed and implemented in our research group for coping with implicit/explicit truth degree annotations, a great variety of connectives and unification by similarity.
A discretized operational semantics for the implementation of Hy-tccp
Gallardo, María del Mar; Panizo, Laura; Titolo, Laura. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
The language Hy-tccp was proposed as an extension of the Timed Concurrent Constraint paradigm (tccp) with continuous time and suitable mechanisms to handle continuous behaviors. This language provides a powerful model for hybrid and cyber-physical systems including concurrency and syn chronization features. In this paper, we propose a discretized operational semantics for Hy-tccp and an extension of the standard LTL to reason about temporal properties of Hy-tccp programs. The semantics and the logics will be the basis for the definition of formal verification and analysis tools, such as model checkers and theorem provers.
A Formal Semantics for Agent Distribution and Fault Tolerance in Jason
Fernández Díaz, Álvaro; Fredlund, Lars-Ake; Benac Earle, Clara; Mariño, Julio. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
This paper provides a formal specification of the distribution and fault-tolerance mechanisms of eJason. The eJason programming language is an extension to the agent-oriented programming language Jason that introduces native support for the transparent distribution of agents as well as fault-tolerance mechanisms. This formal semantics is presented from a multiagent system perspective. It unambiguously describes both the possible evolution of the distributed multi- agent system over time and the different instruments for fault detection and fault recovery, hence exposing their strengths. This specification may serve as a reference for researchers interested in the inclusion of similar mechanisms in agent-oriented programming languages.
A Generic Intermediate Representation for Verification Condition Generation, Work in Progress
Montenegro, Manuel; Peña Marí, Ricardo; Sánchez-Hernández, Jaime. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic internal representation, and how the generated conditions faithfully reflect the semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.
A Haskell Implementation of a Rule-Based Program Transformation for C Programs
Tamarit, Salvador; Vigueras, Guillermo; Carro, Manuel; Mariño, Julio. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
Obtaining good performance when programming heterogeneous computing platforms poses significant challenges for the programmer. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code is transformed into a functionally equivalent one better suited for a given platform. The transformation rules are formalized in a domain-specific language (STML) that takes care of the syntactic and semantic conditions required to apply a given transformation. STML rules are compiled into Haskell function definitions that operate at AST level. Program properties, to be matched with rule conditions, can be automatically inferred or, alternatively, stated as annotations in the source code. Early experimental results are described.
A liberal type system for functional logic programs
López-Fraguas, Francisco J.; Martin-Martin, Enrique; Rodríguez-Hortalá, Juan. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
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.
A Logic of Graph Conditions Extended with Paths
Navarro, Marisa; Orejas, Fernando; Pino, Elvira; Lambers, Leen. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
In this paper we tackle the problem of extending the logic of nested graph conditions with paths. This means, for instance, that we may state properties about the existence of paths between some given nodes. As a main contribution, a sound and complete tableau method is defined for reasoning about this kind of properties.
A SAT-based Efficient Method for the Synthesis from numerical LTL spefications
Rodriguez, Andoni; Sánchez, César. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.
Reactive synthesis is the problem of automatically finding a system that satisfies a temporal logic specification, where the atomic propositions are split into those controlled by the system and those controlled by the environment. In this paper we address the problem of the reactive synthesis of specifications that use numerical variables. We consider an approach that transforms the arithmetic specification into a purely Boolean specification by substituting the arithmetic literals by Boolean variables, and computing an additional Boolean requirement that captures the dependencies between the new variables. The resulting specification can be passed to off-the-self Boolean synthesis tools, and is realizable if and only if the original arithmetic specification is. In this paper, we present a method to compute this equi-realizable Boolean specification based on a nested encoding of the search for such a specification using a SAT-solver (for efficiently encoding the search) and an SMT-solver (for checking the decision power of each player) iteratively.
A Simulation Tool for tccp Programs
Gallardo, María del Mar; Lavado, Leticia; Panizo, Laura. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.
The Timed Concurrent Constraint Language tccp is a declarative synchronous concurrent language, particularly suitable for modelling reactive systems. In tccp, agents communicate and synchronise through a global constraint store. It supports a notion of discrete time that allows all non-blocked agents to proceed with their execution simultaneously. In this paper, we present a modular architecture for the simulation of tccp programs. The tool comprises three main components. First, a set of basic abstract instructions able to model the tccp agent behaviour, the memory model needed to manage the active agents and the state of the store during the execution. Second, the agent interpreter that executes the instructions of the current agent iteratively and calculates the new agents to be executed at the next time instant. Finally, the constraint solver components which are the modules that deal with constraints. In this paper, we describe the implementation of these components and present an example of a real system modelled in tccp.
A System implementing Fuzzy Hypothetical Datalog
Julián Iranzo, Pascual; Sáenz Pérez, Fernando. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
This paper presents a system implementing a novel addition to a fuzzy deductive database: hypothetical queries. Such queries allow users to dynamically make assumptions on a given database instance, either by adding or removing data, without changing the instance. Further, since a fuzzy database includes fuzzy relations, these relations can also be changed with assumptions. This ability for dynamic change seamlessly enables writing “what-if” applications such as decision-support systems. Here, the new language Fuzzy Hypothetical Datalog is presented, along with an operational semantics and stratified inference. It has been implemented in a working system DES readily available on-line. IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), 2020, pp. 1-8, doi: 10.1109/FUZZ48607.2020.9177715.
A Tool for Black-Box Testing in a Multilanguage Verification Platform
Aracil, Marta; García, Pedro; Peña Marí, Ricardo. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.
In the context of the multilanguage verification platform CAVI-ART, we have defined an Intermediate Representation (IR) to which all the source languages are translated. This IR contains both the code and the assertions given by the programmer. Its primary purpose was automatically generating and proving, in a source language independent way, the verification conditions ensuring the program correctness. The logical formulas are sent by the platform to an SMT solver which checks their validity. In this paper we present a new use of the IR: we transform it into an executable language (that it turns out to be Haskell) and also transform the assertions into executable (Haskell) code. Thanks to that, tests can be run on the transformed program, and bugs can be detected either in the specification assertions or in the code. Moreover, we use the assertions to generate black-box test-cases from them, and also as test oracles. In this way, given the IR of a program, all the process ---namely, test-case generation, test running, and test correctness checking--- is completely automatic. So, thousands of tests can be run with little or none effort. The only burden for the programmer is providing the precondition and the postcondition of the code under test, which anyway should have been provided in advance, since the primary goal was to verify the program. We discuss the problems we have encountered while implementing this idea, and how we have solved them. In particular, we report on the use of Haskell resources such as GADTs, efficient data structures, and specialized libraries.
A tool for the automatic generation of logical models of order-sorted first-order theories
Gutiérrez, Raúl; Lucas, Salvador; Reinoso, Patricio. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
Semantics-based program analysis guarantees that the obtained knowledge about focused program features matches the real behaviour of the program. Automation of the analyses requires abstraction mechanisms to approximate the (usually undecidable) program semantics and targeted properties. In this setting, the logical notions of interpretation of a logic language and model of a theory provide an appropriate framework for abstraction in the sense that the corresponding analyses will be sound and, when relying on some decidable theory, amenable for automation. We describe a new tool, AGES, which is able to automatically generate models for order-sorted first-order theories. Such theories are very helpful in the semantic description of most programming languages. The current version of the tool systematically exploits (and relies on) the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of order-sorted signatures and also the (also ranked) predicate symbols in the language by means of appropriately adapted convex matrix interpretations. The system is available as a web application and can be used to give support to users interested in checking properties of software modules provided that they are able to describe the property as an order-sorted first-order theory whose satisfiability guarantees the property. Examples of such properties are partial correctness, program termination, etc. The paper illustrates the use of the tool by means of simple case studies.
A Tutorial on Using Dafny to Construct Verified Software
Lucio, Paqui. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
This paper is a tutorial for newcomers to the field of automated verification tools, though we assume the reader to be relatively familiar with Hoare-style verification. In this paper, besides introducing the most basic features of the language and verifier Dafny, we place special emphasis on how to use Dafny as an assistant in the development of verified programs. Our main aim is to encourage the software engineering community to make the move towards using formal verification tools.
A type derivation system for Erlang
López-Fraguas, Francisco Javier; Montenegro, Manuel; Suárez-García, Gorka. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.
Erlang is a dynamically typed concurrent functional language of increasing interest in industry and academy. Official Erlang distributions come equipped with Dialyzer a useful static analysis tool able to anticipate runtime errors by inferring so-called success types, which are overapproximations to the real semantics of expressions. However, Dialyzer exhibits two main weaknesses: on the practical side, its ability to deal with functions that are typically polymorphic is rather poor; and on the theoretical side, a fully developed theory for its underlying type system –comparable to, say, Hindley-Milner system– does not seem to exist, something that we consider a regrettable circumstance. This work in progress is the starting point of a medium-term project aiming at improving both aspects, so that at its end we should have proposed a full type system able to infer polymorphic success types for Erlang programs, accompanied by solid theoretical foundations including adequateness results for the type system. In this first step we only provide a derivation system of monomorphic success types for Erlang, along with correctness results with respect to a suitable semantics for the language.

Examinar

Examinando Jornadas sobre Programación y Lenguajes (PROLE) por Título

Resultados por página

Opciones de ordenación