Examinando por Materia "JAVA"

Mostrando1 - 6 de 6
  • Ponencia en Congreso
    Analysis of invariants for efficient bounded verification
    (2010-07) Galeotti, Juan Pablo; Rosner, Nicolás; López Pombo, Carlos G.; Frías, Marcelo
    "SAT-based bounded veri cation of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for speci cation violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this article we present TACO, a prototype tool which implements a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate that allows for the parallel, automated computation of tight bounds for Java elds. Experiments show that the translations to propositional formulas require signi cantly less propositional variables, leading in the experiments we have carried out to an improvement on the e ciency of the analysis of orders of magnitude, compared to the non instrumented SAT-based analysis. We show that, in somecases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving."
  • Artículo de Publicación Periódica
    Automated workarounds from Java program specifications based on SAT solving
    (2018-11) Uva, Marcelo; Ponzio, Pablo; Regis, Germán; Aguirre, Nazareno; Frías, Marcelo
    "The failures that bugs in software lead to can sometimes be bypassed by the so-called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Existing approaches to workaround-based system recovery consider workarounds that are produced from equivalent method sequences, utomatically computed from user-provided abstract models, or directly produced from user-provided equivalent sequences of operations. In this paper, we present two techniques for computing workarounds from Java code equipped with formal specifications, that improve previous approaches in two respects. First, the particular state where the failure originated is actively involved in computing workarounds, thus leading to repairs that are more state specific. Second, our techniques automatically compute workarounds on concrete program state characterizations, avoiding abstract software models and user-provided equivalences. The first technique uses SAT solving to compute a sequence of methods that is equivalent to a failing method on a specific failing state, but which can also be generalized to schemas for workaround reuse. The second technique directly exploits SAT to circumvent a failing method, building a state that mimics the (correct) behaviour of a failing routine, from a specific program state too. We perform an experimental evaluation based on case studies involving implementations of collections and a library for date arithmetic, showing that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run-time repairs. Our results also show that our state-specific workarounds enable us to produce repairs in many cases where previous workaround-based approaches are inapplicable."
  • Ponencia en Congreso
    Automated workarounds from Java Program specifications based on SAT solving
    (2017) Uva, Marcelo; Ponzio, Pablo; Regis, Germán; Aguirre, Nazareno; Frías, Marcelo
    "The failures that bugs in software lead to can sometimes be bypassed by the so called workarounds: when a (faulty) routine fails, alternative routines that the system offers can be used in place of the failing one, to circumvent the failure. Previous works have exploited this workarounds notion to automatically recover from runtime failures in some application domains. However, existing approaches that compute workarounds automatically either require the user to manually build an abstract model of the software under consideration, or to provide equivalent sequences of operations from which workarounds are computed, diminishing the automation of workaround-based system recovery. In this paper, we present two techniques that automatically compute workarounds from Java code equipped with formal specifications, avoiding abstract software models and user provided equivalences. These techniques employ SAT solving to compute workarounds on concrete program state characterizations. The first employs SAT solving to compute traditional workarounds, while the second directly exploits SAT solving to circumvent a failing method, building a state that mimics the (correct) behaviour of this failing routine. Our experiments, based on case studies involving implementations of collections and a library for date arithmetic, enable us to show that the techniques can effectively compute workarounds from complex contracts in an important number of cases, in time that makes them feasible to be used for run time repairs."
  • Ponencia en Congreso
    EvoSpex: An evolutionary algorithm for learning postconditions (artifact)
    (2021) Molina, Facundo; Ponzio, Pablo; Aguirre, Nazareno; Frías, Marcelo
    "Having the expected behavior of software specified in a formal language can greatly improve the automation of software verification activities, since these need to contrast the intended behavior with the actual software implementation. Unfortunately, software many times lacks such specifications, and thus providing tools and techniques that can assist developers in the construction of software specifications are relevant in software engineering. As an aid in this context, we present EvoSpex, a tool that given a Java method, automatically produces a specification of the method’s current behavior, in the form of postcondition assertions. EvoSpex is based on generating software runs from the implementation (valid runs), making modifications to the runs to build divergent behaviors (invalid runs), and executing a genetic algorithm that tries to evolve a specification to satisfy the valid runs, and leave out the invalid ones. Our tool supports a rich JML-like assertion language, that can capture complex specifications, including sophisticated object structural properties."
  • Proyecto final de Grado
    Genetic Working Space
    (2017) Ducret, Argentino; Gutiérrez, Ignacio; Parpaglione, María Cristina
    "Genetic working space es una solución con algoritmos genéticos al problema de elegir una distribución de asientos para un conjunto de empleados, sujeto a restricciones. Para su implementación​ ​se​ ​utilizó​ ​un​ ​motor​ ​de​ ​algoritmos​ ​genéticos​ ​desarrollado​ ​en​ ​Java."
  • Ponencia en Congreso
    Towards temporal graph database
    (2016) Campos, Alexander; Mozzino, Jorge; Vaisman, Alejandro Ariel
    "In spite of the extensive literature on graph databases (GDBs), temporal GDBs have not received too much attention so far. Tempo ral GBDs can capture, for example, the evolution of social networks across time, a relevant topic in data analysis nowadays. We propose a data model and query language (denoted TEG-QL) for temporal GDBs, based on the notion of attribute graphs. This allows a straightforward translation to Neo4J, a well-known GBD."