Análisis de programas y verificación
URI permanente para esta colección:
Artículos en la categoría Análisis de programas y verificación publicados en las Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022).
Notificar un error en esta colección
Examinar
Envíos recientes
Artículo A SAT-based Efficient Method for the Synthesis from numerical LTL speficationsRodriguez, 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.Resumen The origins of the halting problemLucas, Salvador. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.The halting problem is a prominent example of undecidable problem and its formulation and undecidability proof is usually attributed to Turing's 1936 landmark paper. Copeland noticed in 2004, though, that it was so named and, apparently, first stated in a 1958 book by Martin Davis. We provide additional arguments partially supporting this claim as follows: (i) with a focus on computable (real) numbers with infinitely many digits (e.g., +A8A), in his paper Turing was not concerned with halting machines+ADs (ii) the two decision problems considered by Turing concern the ability of his machines to produce specific kinds of outputs, rather than reaching a halting state, something which was missing from Turing's notion of computation+ADs and (iii) from 1936 to 1958, when considering the literature of the field no paper refers to any +IBw-halting problem+IB0 of Turing Machines until Davis' book. However, there were important preliminary contributions by (iv) Church, for whom termination was part of his notion of computation (for the +A7s--calculus), and (v) Kleene, who essentially formulated, in his 1952 book, what we know as the halting problem now.Resumen Verified Model Checking for Conjunctive Positive LogicAbuin, Alex; Díaz de Cerio, Unai; Hermo, Montserrat; Lucio, Paqui. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.La referencia completa es: Abuin, A., Díaz de Cerio, U., Hermo, M. and Lucio, P., Verified Model Checking for Conjunctive Positive Logic. SN COMPUTER SCIENCE, VOL 2, Springer 2021. https://doi.org/10.1007/s42979-020-00417-3