Presentaciones a Congresos

Permanent URI for this collection

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

Browse

Now showing 1 - 20 of 51

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.
Models and query languages for temporal property graph database
(2022) Soliani, Valeria
"Although property graphs are increasingly being studied by the research community, most authors do not consider the evolution of such graphs over time. However, this is needed to capture a wide range of real-world situations, where changes normally occur. In this work, we propose a temporal model and a high level query language for property graphs and analyse the real-world cases where they can be useful, with focus on transportation networks (like road and river networks) equipped with sensors that measure different variables over time. Many kinds of interesting paths arise in this scenario. To efficiently compute these paths, also path indexing techniques must be studied."
Modeling and querying sensor networks using temporal graph databases
(2022) Kuijpers, Bart; Soliani, Valeria; Vaisman, Alejandro Ariel
"Transportation networks (e.g., river systems or road net works) equipped with sensors that collect data for several different pur poses can be naturally modeled using graph databases. However, since networks can change over time, to represent these changes appropriately, a temporal graph data model is required. In this paper, we show that sensor-equipped transportation networks can be represented and queried using temporal graph databases and query languages. For this, we extend a recently introduced temporal graph data model and its high-level query language T-GQL to support time series in the nodes of the graph. We redefine temporal paths and study and implement a new kind of path, called Flow path. We take the Flanders’ river system as a use case."
Indexing continuous paths in temporal graphs
(2022) Kuijpers, Bart; Ribas, Ignacio; Soliani, Valeria; Vaisman, Alejandro Ariel
"Temporal property graph databases track the evolution over time of nodes, properties, and edges in graphs. Computing temporal paths in these graphs is hard. In this paper we focus on indexing Continuous Paths, defined as paths that exist continuously during a certain time interval. We propose an index structure called TGIndex where index nodes are defined as nodes in the graph database. Two different indexing strategies are studied. We show how the index is used for querying and also present different search strategies, that are compared and analyzed using a large synthetic graph."
Incorporating coverage criteria in bounded exhaustive black box test generation of structural inputs
(2011) Aguirre, Nazareno; Bengolea, Valeria; Galeotti, Juan Pablo; Frías, Marcelo
"The automated generation of test cases for heap allocated, complex, structures is particularly difficult. Various state of the art tools tackle this problem by bounded exhaustive exploration of potential test cases, using constraint solving mechanisms based on techniques such as search, model checking, symbolic execution and combinations of these. In this article we present a technique for improving the bounded ex haustive constraint based test case generation of structurally complex inputs, for “filtering” approaches. The technique works by guiding the search considering a given black box test criterion. Such a test criterion is incorporated in the constraint based mechanism so that the exploration of potential test cases can be pruned without missing coverable classes of inputs, corresponding to the test criterion. We present the technique, together with some case studies illustrating its performance for some black box testing criteria. The experimental results associated with these case studies are shown in the context of Korat, a state of the art tool for constraint based test case generation, but the approach is applicable in other contexts using a filtering approach to test generation."
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."
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)."
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."
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."
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."
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."
Trajectory sequential patterns with regular expression constraints including spatial queries
(2010-05) Gardella, Pablo; Gómez, Leticia Irene; Vaisman, Alejandro Ariel
"Moving object (MO) data representation and computing have received a fair share of attention over recent years from the database community. Replacing raw trajectory data (i.e., MO positions at different time instants) by sequences of application-dependent stops occurred at so-called places of interest (Pols) leads to the notion of semantic trajectories. Different techniques exist for sequential pattern analysis of trajectories defined in this way. One of them, RE-SPaM, expresses sequential patterns by means of regular expressions built not only over item identifiers, but also over constraints defined on the (temporal and non-temporal) attributes of the items to be analyzed. This analysis could be greatly enriched if spatial and non-spatial data associated with the MO are taken into account. In this paper we show how we can take advantage of the extensibility properties of RE-SPaM to augment its expressive power by allowing to include spatial queries in the constraints. For this, we make use of Piet, a framework allowing to integrate OLAP, GIS and MO data, and its associated query language denoted Piet-QL, providing a link between moving object data and their geographic environment."
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."
Querying semantic web data cubes
(2016) Etcheverry, Lorena; Vaisman, Alejandro Ariel
"We address the problem of querying data cubes for Online Analytical Processing (OLAP) analysis, directly on the Semantic Web (SW). We rst introduce CQL, a simple algebra for querying data cubes at a conceptual level. Taking advantage of QB4OLAP metadata, we automatically translate CQL queries into SPARQL ones, and propose query optimization strategies that adapt, to the particular OLAP set ting, general-purpose techniques. A web application allows exploring and querying OLAP cubes on the SW, using the machinery presented here."
An RDF vocabulary for meta-programming with SPARQL algebra
(2016) Ceriani, Miguel; Vaisman, Alejandro Ariel
"SPARQL queries can be represented in RDF in order to work with them as first-class citizen in Semantic Web applications. The representation used so far, SPIN SPARQL, closely follows the abstract syntax tree, but fails to di rectly capture the semantics and is hard to work with for query rewriting. Here a novel vocabulary based on SPARQL Algebra is presented. The adequacy of the language is empirically shown through a few examples. "
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."
Speckle noise reduction in SAR images using information theory
(2020) Chan, Debora; Gambini, Juliana; Frery, Alejandro C.
"In this work, a new nonlocal means filter for single-look speckled data using the Shannon and Renyi entropies is proposed. The measure of similarity between a central window and patches of the image is based on a statistical test for comparing if two samples have the same entropy and hence have the same distribution. The results are encouraging, as the filtered image has better signal-to-noise ratio, it preserves the mean, and the edges are not severely blurred."
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."
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."
Modelling and querying star and snowflake warehouses using graph databases
(2019) Vaisman, Alejandro Ariel; Besteiro, María Florencia; Valverde Melito, Maximiliano Javier
"In current “Big Data” scenarios, graph databases are increasingly being used. Online Analytical Processing (OLAP) operations can expand the possibilities of graph analysis beyond the traditional graphbased computation. This paper studies graph databases as an alternative to implement star and snowflake schemas, the typical choices for data warehouse design. For this, the MusicBrainz database is used. A data warehouse for this database is designed, and implemented over a Postgres relational database. This warehouse is also represented as a graph, and implemented over the Neo4j graph database. A collection of typical OLAP queries is used to compare both implementations. The results reported here show that in ten out of thirteen queries tested, the graph implementation outperforms the relational one, in ratios that go from 1.3 to 26 times faster, and performs similarly to the relational implementation in the three remaining cases."

Browse

Recent Submissions