PROLE 2023 (Ciudad Real)
URI permantente para esta comunidad:
Las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023) se han celebrado en Ciudad Real del 12 al 14 de septiembre de 2023, como parte de las Jornadas Sistedes.
El programa de PROLE 2023 se ha organizado en torno a sesiones temáticas o tracks.
Examinar
Examinando PROLE 2023 (Ciudad Real) por Fecha de publicación
Mostrando 1 - 20 de 23
Resultados por página
Opciones de ordenación
Artículo Towards a Rewriting-Logic Semantics of PDurán, Francisco; Pozas García, Nicolás; Ramírez, Carlos; Rocha, Camilo. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.P is a programming language based on state machines, suited for the definition of asynchronous event-driven open systems. The language was designed with verification in mind and it is bundled with back-end analysis engines for, e.g., bounded model checking. With the aim of extending such verification capabilities, a semantics of P in rewriting logic has been developed. Given this formal semantics, developed using the rewriting-logic language Maude, the Maude Formal Environment (MFE) can now be used to carry on different types of analyses on P programs. These capabilities are illustrated by carrying on reachability analysis and model checking of P programs.Preliminares PrefacioActas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Prefacio de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)Resumen Building Information Modeling Using Constraint Logic ProgrammingArias, Joaquín; Carro, Manuel. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Joaquín Arias, Seppo Törmä, Manuel Carro, Gopal Gupta: Building Information Modeling Using Constraint Logic Programming. Theory Pract. Log. Program. 22(5): 723-738 (2022) Presentado en ICLP 2022 (Haifa, Israel)Resumen QMaude: quantitative specification and verification in rewriting logicRubio, Rubén; Martí-Oliet, Narciso; Pita, Isabel; Verdejo, Alberto. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.In formal verification, qualitative and quantitative aspects are both relevant, and high-level formalisms are convenient to naturally specify the systems under study and their properties. In this paper, we present a framework for describing probabilistic models on top of nondeterministic specifications in the highly-expressive language Maude, based on rewriting logic. Quantitative properties can be checked and calculated on them using both probabilistic and statistical methods with external tools like PRISM, Storm, MultiVeSta, and custom implementations as backends. At the same time, the underlying nondeterministic system can be verified using the qualitative model-checking and deductive tools already available in Maude.Resumen Modeling and verification of the post-quantum key encapsulation mechanism KYBER using MaudeGarcía, Víctor; Escobar, Santiago; Ogata, Kazuhiro. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Communication and information technologies shape the world’s systems of today, and those systems shape our society. The security of those systems relies on mathematical problems hard to solve for classical computers, that is, the available current computers. Recent advances in quantum computing threaten the security of our systems and the communications we use. In order to face this threat, multiple solutions and protocols have been proposed. Kyber is one of these protocols, and precisely it is a key encapsulation mechanism that bases its security in the learning with errors problem over module lattices. The presented work focuses on the analysis of Kyber to check its security under Dolev-Yao adversary assumptions. For that matter, we first learn about the current state of the solutions proposed against the threat of quantum adversaries and study how Kyber works. In the system-specification language Maude, we then construct a symbolic model to represent the behaviour of Kyber in a network. In this model, we conduct reachability analysis with the s e a r c h command and find that a Man-In-The-Middle attack is present. Then we use the Maude LTL logical model checker to extend the analysis of the system by proving if liveness and security properties hold. Conference name: FAVPQC 2022: International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols. Year of publication: 2022Artículo xeLTL: Extending eLTL with variablesPanizo, Laura; Gallardo, María del Mar. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Our daily activity is increasingly integrated with systems that somehow adapt their behaviour to our state or reactions. These systems are usually called reactive systems since they evolve based on internal or external events produced by their environment. The massive use of smartphones and wearable devices for health monitoring is just an example of how these systems impact in our lives. In addition, some systems, such as those for assisted or autonomous driving, carry out critical tasks. Thus, it is important to ensure that reactive systems satisfy safety requirements in which, in many cases, is relevant the evolution of time or other physical magnitudes. In this paper, we present the eXtended Event-driven Temporal Logic (xeLTL) that can express requirements over intervals of parameterized events.Artículo Fuzzy Retrieval of Linked Open DataAlmendros-Jiménez, Jesus M.; Becerra Terón, Antonio; Moreno, Ginés. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.The technologies associated with the Semantic Web facilitate the publication of Open Data as well as their integration into the Linked Open Data cloud for which RDF format has been chosen. The promoted W3C RDF query language SPARQL became very popular and has been subject of study in recent years, with the goal of improving SPARQL engines in terms of functionality and usability. In this line of research, our research group has developed a fuzzy extension of SPARQL, called FSA-SPARQL (Fuzzy Sets and Aggregators based SPARQL). Here we go a step forward, adapting FSA-SPARQL for querying Linked Open Data with a fuzzy taste. Three goals are pursued, (i) fuzzification of Linked Open Data datasets, (ii) to extend FSA-SPARQL fuzzy aggregation and (iii) to equip FSA-SPARQL with quantification. Fuzzification, that is, interpretation of Linked Open Data datasets as fuzzy sets is made automatically at querying time, using trapezoidal membership functions. Powerful fuzzy aggregation and quantification operators are introduced in FSA-SPARQL based on fuzzy cardinals of fuzzy sets. As a result of the goals, FSA-SPARQL can be used for the retrieval of Linked Open Data datasets in real time, combining fuzzy aggregation and quantification. The proposed extension for FSA-SPARQL has been implemented and the system is available at our Web site.Artículo On the Safe Execution of Symbolic Similarity-based Fuzzy Logic ProgramsMoreno, Ginés; Riaza Valverde, José Antonio. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Introducing “Fuzzy Aggregators and Similarity Into a Logic Language” leads to FASILL, whose symbolic extension (called sFASILL) is able to manage both concrete and unknown (symbolic constants) truth degrees, similarity annotations and fuzzy connectives. The symbolic execution of sFASILL programs helps to guess the impact of such unknown symbols on the outputs before instantiating them with concrete values in program rules and similarity relations. In this paper we reason about the constraints that symbolic substitutions must satisfy in order to preserve the set of fuzzy computed answer obtained at execution time before or after instantiating a given sFASILL program. Based on such safeness conditions, we have formally proved two theoretical results with different levels of generality/practicability for correctly executing symbolic sFASILL and instantiated FASILL programs.Artículo An Open Problem on the Complexity of Realizability for Safety LTL and Related SubfragmentsArteche, Noel; Hermo, Montserrat. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.We study the realizability problem for Safety LTL, the syntactic fragment of Linear Temporal Logic capturing safe formulas. It is known that realizability for formulas in this fragment is EXP-hard, and the best-known upper bound is 2EXP. In this work, we approach the exact classification of the complexity of realizability for Safety LTL by studying seemingly weaker subfragments. In particular, we study the fragment consisting of formulas of the form α ∧ Gψ, where α is a present formula over system variables and ψ contains Next as the only temporal operator. We prove that the realizability problem for this new fragment, which we call GX_0, is also EXP-complete, and observe that this fragment is equirealizable to existing more expressive fragments, such as the LTL_EBR system of Cimatti et al.[8]. We show how trying to prove equirealizability between the full Safety LTL and the existing EXP-complete fragments fails. We highlight the practical relevance of fast algorithms for Safety LTL and point at the open problem of providing a tighter bound on the exact computational complexity of realizability for the full Safety LTL fragment.Resumen Canonical Narrowing for Variant-Based Conditional Rewrite TheoriesLópez Rueda, Raúl; Escobar, Santiago. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.23rd International Conference on Formal Engineering Methods (ICFEM 2022). Madrid, Spain: Springer. Maude currently supports many symbolic reasoning features such as order-sorted equational unification and order-sorted narrowingbased symbolic reachability analysis. There have been many advances and new features added to improve narrowing in Maude but only at a theoretical level. In this paper, we provide a very elegant, transparent, and extremely pragmatic approach for conditional rewrite theories where the conditions are just equalities solved by equational unification. We show how two conditional theories, never executed before, are now executable with very good performance.We also show how real execution works better than the manually transformed version.Artículo Grafos para fragmentación de programas sensible a los campos que mejoran al usarlosGalindo, Carlos; Pérez Rubio, Sergio; Sílva, Josep. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.El nivel de granularidad que proporciona el Program Dependence Graph (PDG) al representar estructuras de datos complejas (listas, arrays, objetos...) es insuficiente para diferenciar entre sus elementos al aplicar fragmentación de programas. En un trabajo anterior, se propuso un nuevo modelo, el Constrained-Edges Program Dependence Graph (CE-PDG), capaz de obtener fragmentos precisos al aplicar fragmentación a programas con estructuras de datos recursivas. En este trabajo, mostramos cómo los mecanismos utilizados por el CE-PDG pueden ser mejorados, proporcionando fragmentos notablemente más precisos de una manera más eficiente. Estas mejoras implican dos cambios distintos sobre el proceso de fragmentación: un nuevo criterio de parada para el algoritmo y una sustitución permanente en las restricciones del CE-PDG que mejora la eficiencia del recorrido cuantos más fragmentos se calculan sobre el grafo.Artículo Nostralangus: Prophecy-based programmingCeresa, Martin; Sánchez, César. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.In this work in progress, we explore the possibility of having a new operator capable of bringing information about the system in the future. While previous works define \emph{prophecy variables} as a way of inspecting the state of the system in the future, we propose to write programs that can actively use such information to choose what agents can do now. Verification techniques define systems where no \textbf{paradoxes} can be introduced but information from the future is still accessible to us as verifiers. In this document, we liberate the programs of such restriction equipping programs with a prophetic conditional operation: \(\ \, \mathcal{P}(\Phi) \, \ \, \mathcal{A} \, \ \, \mathcal{B}\). Actions \(\mathcal{A}\) and \(\mathcal{B}\) are executed depending on a future predicate \(\Phi\) about the system. Both sets of actions \(\mathcal{A}\) and \(\mathcal{B}\) can contradict the prophecy creating paradoxes. We explore how we can rule out some paradoxes appealing to different execution systems and two interpretations of prophecies. One of \emph{possible worlds} where making a prediction generates two possible worlds, one on which the prediction is true and another on which is false. Another interpretation in which the time is linearized using a try-catch interpretation.Artículo Problemas de confluencia en transformación de grafos: de los pares críticos a los conflictos iniciales.Orejas, Fernando. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Mucha gente cree que la transformación de grafos no es nada más que una generalización de la reescritura de términos. Sin embargo, en este tutorial vetemos que la técnica que se usa en reescritura de términos para la comprobación de la confluencia, el cálculo de los pares críticos y la comprobación de su convergencia, genera problemas serios cuando se adapta a la transformación de grafos. Adicionalmente, veremos cómo se resuelven, en mayor o menor medida, estos problemas a traves del nuevo concepto de conflicto inicial.Resumen Bousi∼Prolog: Design and implementation of a proximity-based fuzzy logic programming language.Julián Iranzo, Pascual; Sáenz Pérez, Fernando. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.The fuzzy logic programming language Bousi∼Prolog extends Prolog with a weak unification algorithm based on proximity relations and truth degree annotations. The weak unification algorithm makes the search for answers more flexible, while rule annotations make possible knowledge-based applications where the rules may be uncertain. In this paper, after recalling the main concepts supporting this language, we detail its design and implementation. We describe the implementation of its operational semantics, which is based on compiling programs and queries into Prolog, and those important features that makes it more applicable: fuzzy sets, integration with WordNet and efficiency techniques. The result is a high-level open-source implementation of the Bousi∼Prolog system, written on top of SWI-Prolog, and publicly available. We also summarise some experiments measuring its performance compared to other systems. [Work already published: Expert Syst. Appl. 213(Part): 118858 (2023) ]Resumen Proving and disproving confluence of context-sensitive rewritingLucas, Salvador; Vítores, Miguel; Gutiérrez, Raúl. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Context-sensitive rewriting is a restriction of term rewriting where reductions are allowed on specific arguments of function symbols only, and then in particular positions of terms. Confluence is an abstract property of reduction relations guaranteeing that two diverging reduction sequences can always be joined into a common reduct. In this paper we investigate confluence of context-sensitive rewriting and present some novel results. In particular, a characterization of local confluence of context-sensitive rewriting as the joinability of an extended class of critical pairs which we introduce here. We also show that the treatment of joinability of critical pairs using theorem proving and solving feasibility problems is useful to automatically prove and disprove confluence of context-sensitive rewriting. Our techniques have been implemented in a new tool, CONFident. We show by means of benchmarks the impact of the new techniques discussed in the paper.Preliminares ComitésActas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Presidentes, coordinadores y comités de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)Artículo Indecidibilidad del análisis de dependencias de datosGalindo, Carlos; Pérez Rubio, Sergio; Sílva, Josep. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Los análisis de dependencias de datos (ADD) responden a la pregunta: ¿qué partes del programa pueden influenciar el valor de esta variable? Estos análisis son comunes en herramientas como compiladores, depuradores y muchos otros análisis de software para determinar terminación, paralelizar automáticamente, depurar, optimizar, etc. Sabemos que en el caso general ADD es indecidible debido a la no-terminación: siempre es posible encontrar un programa para el que no podemos asegurar si la variable de interés es alcanzable (el programa podría divergir antes), y por tanto no podemos determinar si alguna parte del programa podría influenciar a esa variable. En enero del 2000, Thomas Reps probó la indecidibilidad de un ADD para programas que sí terminan, demostrando que la no-terminación no es la única causa fundamental de indecidibilidad. El ADD que Reps utilizó, sin embargo, era un análisis muy específico. Este trabajo utiliza y expande los resultados de Reps para determinar que existe una clase de ADDs (que incluye el propio ADD usado por Reps) que son indecidibles incluso para programas que sí terminan. Además, describimos qué características debe tener un lenguaje de programación para que los ADDs de esta clase sean indecidibles en el caso general.Artículo Towards an Efficient Implementation of Tableaux for Reactive Safety SpecificationsAlonso, Ander; Hermo, Montserrat; Oca, Josu. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.In this article, we take the first steps to implement a tableau method for deciding realizability of specifications expressed in a safety fragment of linear temporal logic. This tableau method also allows us to extract (i.e., synthesize) a correct system in the case the specification is realizable. In particular, we explain here how to efficiently implement a new normal form called terse normal form, which is crucial to the development of such tableau method.Resumen Executable Contracts for ElixirPérez Rubio, Sergio; Bueso de Barrio, Luis Eduardo; Ballesteros González, Ignacio; Herranz, Angel; Mariño, Julio; Benac Earle, Clara; Fredlund, Lars-Ake. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.This paper introduces a new library for implementing executable contracts in Elixir. In addition to classical contract constructs such as preconditions and postconditions, the library permits e.g. to specify exceptional behaviour (i.e. which exceptions are thrown and under which conditions), and to associate timers with function calls to detect non-terminating or too slow computations.Artículo Work in Progress: Generation of Algebraic Data Types using Evolutionary AlgorithmsBallesteros González, Ignacio; Benac Earle, Clara; Fredlund, Lars-Ake; Herranz, Angel; Mariño, Julio. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.Automatic data generation is a key component of automated software testing. Random generation of test input data can uncover some bugs in software, but its effectiveness decreases when those inputs must satisfy complex properties in order to be meaningful. In this work we study an evolutionary approach to generate values that can be encoded as algebraic data types plus additional properties. More specifically, we have conducted an experiment on the automated generation of red-black trees using evolutionary algorithms. Although relatively simple, this example will allow us to introduce the main principles of evolutionary algorithms and how these principles can be applied to obtain valid, nontrivial samples of a given data structure. While the preliminary results show some potential, further experimentation is needed.