DSpace Repository :: Browsing by Author "Ponzio, Pablo"

Browsing by Author "Ponzio, Pablo"

Now showing 1 - 8 of 8

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."
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."
Automatically identifying sufficient object builders from Module APIs
(2019) Ponzio, Pablo; Bengolea, Valeria; Politano, Mariano; Aguirre, Nazareno; Frías, Marcelo
"Various approaches to software analysis (e.g. test input generation, software model checking) require engineers to (manually) identify a subset of a module’s methods in order to drive the analysis. Given a module to be analyzed, engineers typically select a subset of its methods to be considered as object builders to define a so-called driver, that will be used to automatically build objects for analysis, e.g., combining them non-deterministically, randomly, etc. This requires a careful inspection of the module and its API, since both the relative exhaustiveness of the analysis (leaving important methods out may systematically avoid generating different objects), as well as its efficiency (the different bounded combinations of methods grows exponentially as the number of methods increases), are affected by the selection. We propose an approach for automatically selecting a set of builders from a module’s API, based on an evolutionary algorithm that favors sets of methods whose combinations lead to producing larger sets of objects. The algorithm also takes into account other characteristics of these sets of methods, trying to prioritize the selection of methods with less and simpler parameters. As the implementation of this evolutionary mechanism requires in principle handling and comparing large sets of objects, and this grows very quickly both in terms of space and running times, we employ an abstraction of sets of objects, called field extensions, that involves using the field values of the objects in the set instead of the actual objects, and enables us to effectively implement our mechanism. An experimental assessment on a benchmark of stateful classes shows that our approach can automatically identify sets of builders that are sufficient (can be used to create any instance of the module) and minimal (do not contain superfluous methods), in a reasonable time."
DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
(2017-09) Regis, Germán; Cornejo, César; Gutiérrez Brida, Simón; Politano, Mariano; Raverta, Fernando; Ponzio, Pablo; Aguirre, Nazareno; Galeotti, Juan Pablo; Frías, Marcelo
"We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy."
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."
Improving lazy abstraction for SCR specifications through constraint relaxation
(2018-03) Degiovanni, Renzo; Ponzio, Pablo; Aguirre, Nazareno; Frías, Marcelo
"Formal requirements specifications, eg, software cost reduction (SCR) specifications, are challenging to analyse using automated techniques such as model checking. Since such specifications are meant to capture requirements, they tend to refer to real-world magnitudes often characterized through variables over large domains. At the same time, they feature a high degree of nondeterminism, as opposed to other analysis contexts such as (sequential) program verification. This makes model checking of SCR specifications difficult even for symbolic approaches. Moreover, automated abstraction refinement techniques such as counterexample guided abstraction refinement fail in many cases in this context, since the concrete state space is typically large, and reaching specific states of interest may require complex executions involving many different states, causing these approaches to perform many abstraction refinements, and making them ineffective in practice. In this paper, an approach to tackle the above situation, through a 2-stage abstraction, is presented. The specification is first relaxed, by disregarding the constraints imposed in the specification by physical laws or by the environment, before being fed to a counterexample guided abstraction refinement procedure, tailored to SCR. By relaxing the original specification, shorter spurious counterexamples are produced, favouring the abstraction refinement through the introduction of fewer abstraction predicates. Then, when a counterexample is concretizable with respect to the relaxed (concrete) specification but it is spurious with respect to the original specification, an efficient though incomplete refinement step is applied to the constraints, to cause the removal of the spurious case. This approach is experimentally assessed, comparing it with related techniques in the verification of properties and in automated test case generation, using various SCR specifications drawn from the literature as case studies. The experiments show that this new approach runs faster and scales better to larger, more complex specifications than related techniques."
On the effect of object redundancy elimination in randomly testing collection classes
(2018-05) Ponzio, Pablo; Bengolea, Valeria; Gutiérrez Brida, Simón; Scilingo, Gastón; Aguirre, Nazareno; Frías, Marcelo
"In this paper, we analyze the effect of reducing object redundancy in random testing, by comparing the Randoop random testing tool with a version of the tool that disregards tests that only produce objects that have been previously generated by other tests. As a side effect, this variant also identifies methods in the software under test that never participate in state changes, and uses these more heavily when building assertions. Our evaluation of this strategy concentrates on collection classes, since in this context of object-oriented implementations that describe stateful objects obbeying complex invariants, object variability is highly relevant. Our experimental comparison takes the main data structures in java.util, and shows that our object redundancy reduction strategy has an important impact in testing collections, measured in terms of code coverage and mutation killing."
Training binary classifiers as data structure invariants
(2019-05) Molina, Facundo; Degiovanni, Renzo; Ponzio, Pablo; Regis, Germán; Aguirre, Nazareno; Frías, Marcelo
"We present a technique to distinguish valid from invalid data structure objects. The technique is based on building an artificial neural network, more precisely a binary classifier, and training it to identify valid and invalid instances of a data structure. The obtained classifier can then be used in place of the data structure’s invariant, in order to attempt to identify (in)correct behaviors in programs manipulating the structure. In order to produce the valid objects to train the network, an assumed-correct set of object building routines is randomly executed. Invalid instances are produced by generating values for object fields that “break” the collected valid values, i.e., that assign values to object fields that have not been observed as feasible in the assumed-correct executions that led to the collected valid instances. We experimentally assess this approach, over a benchmark of data structures.We show that this learning technique produces classifiers that achieve significantly better accuracy in classifying valid/invalid objects compared to a technique for dynamic invariant detection, and leads to improved bug finding."

Browsing by Author "Ponzio, Pablo"

Results Per Page

Sort Options