Presentaciones a Congresos

Permanent URI for this collection

http://ri.itba.edu.ar/handle/123456789/64

Browse

Now showing 1 - 20 of 51

Aggregation languages for moving object and places of interest
(2008) Gómez, Leticia Irene; Kuijpers, Bart; Vaisman, Alejandro Ariel
"We address aggregate queries over GIS data and moving object data, where non-spatial information is stored in a data warehouse. We propose a formal data model and query language to express complex aggregate queries. Next, we study the compression of trajectory data, produced by moving objects, using the notions of stops and moves. We show that stops and moves are expressible in our query language and we consider a fragment of this language, consisting of regular expressions to talk about temporally ordered sequences of stops and moves. This fragment can be used not only for querying, but also for expressing data mining and pattern matching tasks over trajectory data."
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."
An analysis of the suitability of test-based patch acceptance criteria
(2017-07) Zemín, Luciano; Gutiérrez Brida, Simón; Godio, Ariel; Cornejo, César; Degiovanni, Renzo; Regis, Germán; Aguirre, Nazareno; Frías, Marcelo
"Program repair techniques attempt to fix programs by looking for patches within a search space of fix candidates. These techniques require a specification of the program to be repaired, used as an acceptance criterion for fix candidates, that often also plays an important role in guiding some search processes. Most tools use tests as specifications, which constitutes a risk, since the incompleteness of tests as specifications may lead one to obtain spurious repairs, that pass all tests but are in fact incorrect. This problem has been identified by various researchers, raising concerns about the validity of program fixes. More thorough studies have been proposed using different sets of tests for fix validation, and resorting to manual inspection, showing that while tools reduce their program fixing rate, they are still able to repair a significant number of cases. In this paper, we perform a different analysis of the suitability of tests as acceptance criteria for automated program fixes, by checking patches produced by automated repair tools using a bug-finding tool, as opposed to previous works that used tests or manual inspections. We develop a number of experiments in which faulty programs from a known benchmark are fed to the program repair tools GenProg, Angelix, AutoFix and Nopol, using test suites of varying quality and extension, including those accompanying the benchmark. We then check the produced patches against formal specifications using a bug-finding tool. Our results show that, in general, automated program repair tools are significantly more likely to accept a spurious program fix than producing an actual one, in the studied scenarios. "
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."
Bounded exhaustive search of alloy specification repairs
(2021) Gutiérrez Brida, Simón; Regis, Germán; Zheng, Guolong; Bagher, Hamid; Nguyen, Thanh Vu; Aguirre, Nazareno; Frías, Marcelo
"The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite significant advances in the program repair of imperative languages, there is a dearth of repair techniques for declarative languages. This paper presents BeAFix, an automated repair technique for faulty models written in Alloy, a declarative language based on first-order relational logic. BeAFix is backed with a novel strategy for bounded exhaustive, yet scalable, ex ploration of the spaces of fix candidates and a formally rigorous, sound pruning of such spaces. Moreover, different from the state of-the-art in Alloy automated repair, that relies on the availability of unit tests, BeAFix does not require tests and can work with assertions that are naturally used in formal declarative languages. Our experience with using BeAFix to repair thousands of real world faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art."
Clasificación de Imágenes SAR utilizando descriptores de textura
(2021-10) Gambini, Juliana; Rey, Andrea; Delrieux, Claudio
"Las imágenes SAR (Sythetic Aperture Radar) y PolSAR (Polarimetric Synthetic Aperture Radar) cumplen un rol fundamental en el monitoreo ambiental y observación terrestre debido a que proveen información que las imágenes ópticas no proporcionan. Sin embargo, estas imágenes están contaminadas con un ruido inherente al méetodo de captura llamado ruido speckle que dificulta su análisis e interpretación automática. Los modelos avanzados de segmentación de imágenes SAR están dedicados a resolver las dificultades que este ruido provoca. En este sentido, resulta de suma importancia el estudio de parámetros que describan las características estructurales de textura de imagen en presencia de ruido speckle y permitan su interpretación automática. En este trabajo, se propone un nuevo modelo de clasificación de imágenes SAR basado en el cálculo de descriptores de textura locales, formando un vector característico, el cual involucra estimaciones de parámetros de una distribución de probabilidad, estimaciones de la dimensión fractal y entropía de Tsallis. Luego, el etiquetado de cada pixel se realiza utilizando el método de clasificación supervisada SVM (Support Vector Machine). Se analizan los resultados de aplicar el algoritmo propuesto en imágenes SAR sintéticas, simples y con valores extremos agregados, los cuales resultan altamente prometedores para aplicarse en imágenes reales."
Complete calculi for structured specifications in fork algebra
(2010) López Pombo, Carlos Gustavo; Frías, Marcelo
"In previous articles we presented Argentum, a tool for reasoning across heterogeneous specifications based on the language of fork algebras. Argentum’s foundations were formalized in the framework of institutions. The formalization made simple to describe a methodology capable of producing a complete system desription from partial views, eventually written in different logical languages. Structured specifications were introduced by Sannella and Tarlecki and extensively studied by Borzyszkowski. The latter also presented conditions under which the calculus for structured specifications is complete. Using fork algebras as a “universal” institution capable of representing expressive logics (such as dynamic and temporal logics), requires using a fork language that includes a reflexive-transitive closure operator. The calculus thus obtained does not meet the conditions required by Borzyszkowski. In this article we present structure building operators (SBOs) over fork algebras, and provide a complete calculus for these operators."
Conceptualization maturity metrics for expert systems
(2006) Britos, Paola Verónica; García Martínez, Ramón; Hauge, Ødwin
“Metrics used on development of expert systems is not a well investigated problem area. This article suggests some metrics to be used to measure the maturity of the conceptualization process and the complexity of the decision process in the problem domain. We propose some further work to be done with these metrics. Applying those metrics makes new and interesting problems, concerning the structure of knowledge to surface.”
Data quality in a big data context
(2018) Arolfo, Franco A.; Vaisman, Alejandro Ariel
"In each of the phases of a Big Data analysis process, data quality (DQ) plays a key role. Given the particular characteristics of the data at hand, the traditional DQ methods used for relational databases, based on quality dimensions and metrics, must be adapted and extended, in order to capture the new characteristics that Big Data introduces. This paper dives into this problem, re-defining the DQ dimensions and metrics for a Big Data scenario, where data may arrive, for example, as unstructured documents in real time. This general scenario is instantiated to study the concrete case of Twitter feeds. Further, the paper also describes the implementation of a system that acquires tweets in real time, and computes the quality of each tweet, applying the quality metrics that are defined formally in the paper. The implementation includes a web user interface that allows filtering the tweets for example by keywords, and visualizing the quality of a data stream in many different ways. Experiments are performed and their results discussed."
Detection of breast lesions in medical digital imaging using neural networks
(2006) Ferrero, Gustavo; Britos, Paola Verónica; García Martínez, Ramón
"The purpose of this article is to present an experimental application for the detection of possible breast lesions by means of neural networks in medical digital imaging. This application broadens the scope of research into the creation of different types of topologies with the aim of improving existing networks and creating new architectures which allow for improved detection."
Discovering sensing capability in multi-agent systems
(2010) Parpaglione, María Cristina; Santos, Juan Miguel
"What should be the sensing capabilities of agents in a Multi-Agent System be to solve a problem efficiently, quickly and economicly? This question often appears when trying to solve a problem using Multi-Agent Systems. This paper introduces a method to find these sensing capabilities in order to solve a given problem. To achieve this, the sensing capability of an agent is modeled by a parametrized function and then Genetic Algorithms are used to find the parameters’ values. The individual behavior of the agents are found with Reinforcement Learning."
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."
Equilivest: A robotic vest to aid in post-stroke dynamic balance rehabilitation
(2023-01) Paviotti, Franco; Buniak, Esteban; Ramele, Rodrigo; Freixes, Orestes; Santos, Juan Miguel
Brain stroke is a devastating medical condition, that affects world population and is the main cause of disabilities worldwide. Disabilities related to stroke can affect motor pathways, and may lead to several motor function disorders. One important aspect of motor function is balance which is the ability to control the body’s center of mass inside the base support provided by the lower limb. Stroke can affect dynamic balance as well, which is manifested while walking, impairing autonomy and independence, important factors in Activities of Daily Living (ADL) particularly for young patients.
Evaluación del error en la detección de puntos de borde en imágenes SAR polarimétricas
(2017-04) Monferrán, Daniel; Gambini, Juliana; Frery, Alejandro C.
"El Radar de Apertura Sintética polarimétrico (PolSAR - Polarimentric Synthetic Aperture Radar) es ampliamente utilizado en teledetección porque permite capturar imágenes terrestres de alta resolución. La interpretación automática de imágenes PolSAR es una tarea muy difícil porque éstas contienen un gran volumen de información y además se encuentran contaminadas con ruido speckle. Las características de este ruido hacen necesario utilizar métodos estadísticos para el procesamiento digital de este tipo de imágenes. En esta línea de investigación se pretende evaluar el error que se comete al calcular las posiciones de los puntos de borde dentro de la imagen, utilizando la distribución Wishart compleja y experimentos de Montecarlo en imágenes PolSAR simuladas."
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."
FLACK: Counterexample-guided fault localization for alloy models
(2021) Zheng, Guolong; Nguyen, Thanh Vu; Gutiérrez Brida, Simón; Regis, Germán; Frías, Marcelo; Aguirre, Nazareno; Bagher, Hamid
"Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements. In this work, we introduce a fault localization approach for models written in a declarative language, where the models are not “executed,” but rather converted into a logical formula and solved using backend constraint solvers. We present FLACK, a tool that takes as input an Alloy model consisting of some violated assertion and returns a ranked list of suspicious expressions contributing to the assertion violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion, and instances that do satisfy the assertion to find suspicious expressions in the input model. The experimental results show that FLACK is efficient (can handle complex, real world Alloy models with thousand lines of code within 5 seconds), accurate (can consistently rank buggy expressions in the top 1.9% of the suspicious list), and useful (can often narrow down the error to the exact location within the suspicious expressions)."
From conceptual to logical ETL design using BPMN and relational algebra
(2019) Awiti, Judith; Vaisman, Alejandro Ariel; Zimányi, Esteban
"Extraction, transformation, and loading (ETL) processes are used to extract data from internal and external sources of an organization, transform these data, and load them into a data warehouse. The Business Process Modeling Notation (BPMN) has been proposed for expressing ETL processes at a conceptual level. This paper extends relational algebra (RA) with update operations for specifying ETL processes at a logical level. In this approach, data tasks can be automatically translated into SQL queries to be executed over a DBMS. An extension of RA is presented, as well as a translation mechanism from BPMN to the RA specification. Throughout the paper, the TPC-DI benchmark is used for comparing both approaches. Experiments show the efficiency of the resulting ETL flow with respect to the Pentaho Data Integration tool."
From operational to declarative specifications using a genetic algorithm
(2018-05) Molina, Facundo; Degiovanni, Renzo; Regis, Germán; Castro, Pablo; Aguirre, Nazareno; Frías, Marcelo
"In specification-based test generation, sometimes having a formal specification is not sufficient, since the specification may be in a different formalism from that required by the generation approach being used. In this paper, we deal with this problem specifically in the context in which, while having a formal specification in the form of an operational invariant written in a sequential programming language, one needs, for test generation, a declarative invariant in a logical formalism. We propose a genetic algorithm that given a catalog of common properties of invariants, such as acyclicity, sortedness and balance, attempts to evolve a conjunction of these that most accurately approximates an original operational specification. We present some details of the algorithm, and an experimental evaluation based on a benchmark of data structures, for which we evolve declarative logical invariants from operational ones."
Fusion of magnetic and WiFi fingerprints for indoor positioning
(2018) Grisales Campeón, Juan Pablo; López, Sebastián; de Jesús Meleán, Sergio R.; Moldovan, Horatiu; Parisi, Daniel; Fierens, Pablo Ignacio
"WiFi received signal strength (RSS) and magnetic field intensity are common measures for indoor localization because they are readily available on most mobile devices. There is a vast literature on smartphone positioning using RSS and it has been widely implemented in real-world scenarios in the last two decades. There is much work done on localization aided by magnetic field measurements. We have recently evaluated the accuracy of RSS-based positioning applying state-of-the-art algorithms to measurements in a well-controlled experimental setup. In this paper, we extend this work to assess the accuracy improvements achievable by fusing WiFi and magnetic field information. We show that accuracy improvements of up to 30% are possible."

Browse

Browsing Presentaciones a Congresos by Title

Results Per Page

Sort Options