Showing 1–29 of 29 results for author: Menezes, R

ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST

Authors: Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha, Franz Brauße, Rafael S. Menezes, Konstantin Korovin, Lucas C. Cordeiro

Abstract: This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a new Clang-based C++ front-end to address the challenges posed by modern C++ programs. Although the new front-end has demonstrated significant potential in previous studies, it remains in the developmental stage and lack… ▽ More This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a new Clang-based C++ front-end to address the challenges posed by modern C++ programs. Although the new front-end has demonstrated significant potential in previous studies, it remains in the developmental stage and lacks several essential features. ESBMC v7.6 further enhanced this foundation by adding and extending features based on the Clang AST, such as 1) exception handling, 2) extended memory management and memory safety verification, including dangling pointers, duplicate deallocation, memory leaks and rvalue references and 3) new operational models for STL updating the outdated C++ operational models. Our extensive experiments demonstrate that ESBMC v7.6 can handle a significantly broader range of C++ features introduced in recent versions of the C++ standard. △ Less

Submitted 25 June, 2024; originally announced June 2024.

Comments: 27 pages, 2 figures. arXiv admin note: substantial text overlap with arXiv:2308.05649

Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study

Authors: Rafael Sá Menezes, Edoardo Manino, Fedor Shmarov, Mohannad Aldughaim, Rosiane de Freitas, Lucas C. Cordeiro

Abstract: Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significan… ▽ More Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks. △ Less

Submitted 21 June, 2024; originally announced June 2024.

Comments: Submitted to IFM

Environmental Insights: Democratizing Access to Ambient Air Pollution Data and Predictive Analytics with an Open-Source Python Package

Authors: Liam J Berrisford, Ronaldo Menezes

Abstract: Ambient air pollution is a pervasive issue with wide-ranging effects on human health, ecosystem vitality, and economic structures. Utilizing data on ambient air pollution concentrations, researchers can perform comprehensive analyses to uncover the multifaceted impacts of air pollution across society. To this end, we introduce Environmental Insights, an open-source Python package designed to democ… ▽ More Ambient air pollution is a pervasive issue with wide-ranging effects on human health, ecosystem vitality, and economic structures. Utilizing data on ambient air pollution concentrations, researchers can perform comprehensive analyses to uncover the multifaceted impacts of air pollution across society. To this end, we introduce Environmental Insights, an open-source Python package designed to democratize access to air pollution concentration data. This tool enables users to easily retrieve historical air pollution data and employ a Machine Learning model for forecasting potential future conditions. Moreover, Environmental Insights includes a suite of tools aimed at facilitating the dissemination of analytical findings and enhancing user engagement through dynamic visualizations. This comprehensive approach ensures that the package caters to the diverse needs of individuals looking to explore and understand air pollution trends and their implications. △ Less

Submitted 6 March, 2024; originally announced March 2024.

Comments: 16 pages, 8 figures, 1 table

A Data-Driven Supervised Machine Learning Approach to Estimating Global Ambient Air Pollution Concentrations With Associated Prediction Intervals

Authors: Liam J Berrisford, Hugo Barbosa, Ronaldo Menezes

Abstract: Global ambient air pollution, a transboundary challenge, is typically addressed through interventions relying on data from spatially sparse and heterogeneously placed monitoring stations. These stations often encounter temporal data gaps due to issues such as power outages. In response, we have developed a scalable, data-driven, supervised machine learning framework. This model is designed to impu… ▽ More Global ambient air pollution, a transboundary challenge, is typically addressed through interventions relying on data from spatially sparse and heterogeneously placed monitoring stations. These stations often encounter temporal data gaps due to issues such as power outages. In response, we have developed a scalable, data-driven, supervised machine learning framework. This model is designed to impute missing temporal and spatial measurements, thereby generating a comprehensive dataset for pollutants including NO$_2$, O$_3$, PM$_{10}$, PM$_{2.5}$, and SO$_2$. The dataset, with a fine granularity of 0.25$^{\circ}$ at hourly intervals and accompanied by prediction intervals for each estimate, caters to a wide range of stakeholders relying on outdoor air pollution data for downstream assessments. This enables more detailed studies. Additionally, the model's performance across various geographical locations is examined, providing insights and recommendations for strategic placement of future monitoring stations to further enhance the model's accuracy. △ Less

Submitted 15 February, 2024; originally announced February 2024.

Comments: Main Paper: 25 pages, 15 figures, 5 tables. Supplementary: 4 pages, 3 figures

A Framework for Scalable Ambient Air Pollution Concentration Estimation

Authors: Liam J Berrisford, Lucy S Neal, Helen J Buttery, Benjamin R Evans, Ronaldo Menezes

Abstract: Ambient air pollution remains a critical issue in the United Kingdom, where data on air pollution concentrations form the foundation for interventions aimed at improving air quality. However, the current air pollution monitoring station network in the UK is characterized by spatial sparsity, heterogeneous placement, and frequent temporal data gaps, often due to issues such as power outages. We int… ▽ More Ambient air pollution remains a critical issue in the United Kingdom, where data on air pollution concentrations form the foundation for interventions aimed at improving air quality. However, the current air pollution monitoring station network in the UK is characterized by spatial sparsity, heterogeneous placement, and frequent temporal data gaps, often due to issues such as power outages. We introduce a scalable data-driven supervised machine learning model framework designed to address temporal and spatial data gaps by filling missing measurements. This approach provides a comprehensive dataset for England throughout 2018 at a 1kmx1km hourly resolution. Leveraging machine learning techniques and real-world data from the sparsely distributed monitoring stations, we generate 355,827 synthetic monitoring stations across the study area, yielding data valued at approximately \pounds70 billion. Validation was conducted to assess the model's performance in forecasting, estimating missing locations, and capturing peak concentrations. The resulting dataset is of particular interest to a diverse range of stakeholders engaged in downstream assessments supported by outdoor air pollution concentration data for NO2, O3, PM10, PM2.5, and SO2. This resource empowers stakeholders to conduct studies at a higher resolution than was previously possible. △ Less

Submitted 16 January, 2024; originally announced January 2024.

Comments: Main: 27 pages, 11 figures, 6 tables. Supplementary: 32 pages, 21 figures, 11 tables

ESBMC v7.4: Harnessing the Power of Intervals

Authors: Rafael Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brauße, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas C. Cordeiro

Abstract: ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backw… ▽ More ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backward contractors, and particular optimizations related to singleton intervals because of their ubiquity. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable. △ Less

Submitted 22 December, 2023; originally announced December 2023.

NeuroCodeBench: a plain C neural network benchmark for software verification

Authors: Edoardo Manino, Rafael Sá Menezes, Fedor Shmarov, Lucas C. Cordeiro

Abstract: Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal, they cannot prove the absence of software faults in the network implementation. This paper presents NeuroCodeBench - a verification benchmark for neural network code written in plain C. It contains 32 neural networks wi… ▽ More Safety-critical systems with neural network components require strong guarantees. While existing neural network verification techniques have shown great progress towards this goal, they cannot prove the absence of software faults in the network implementation. This paper presents NeuroCodeBench - a verification benchmark for neural network code written in plain C. It contains 32 neural networks with 607 safety properties divided into 6 categories: maths library, activation functions, error-correcting networks, transfer function approximation, probability density estimation and reinforcement learning. Our preliminary evaluation shows that state-of-the-art software verifiers struggle to provide correct verdicts, due to their incomplete support of the standard C mathematical library and the complexity of larger neural networks. △ Less

Submitted 7 September, 2023; originally announced September 2023.

Comments: Submitted to the 2023 AFRiTS workshop

ESBMC v7.3: Model Checking C++ Programs using Clang AST

Authors: Kunjian Song, Mikhail R. Gadelha, Franz Brauße, Rafael S. Menezes, Lucas C. Cordeiro

Abstract: This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new clang-based C++ front-end. While the previous CPROVER-based front-end served well for handling C++03 programs, it encountered challenges kee** up with the evolving C++ language. As new language and library features were added in each C++ version, the limitations of… ▽ More This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new clang-based C++ front-end. While the previous CPROVER-based front-end served well for handling C++03 programs, it encountered challenges kee** up with the evolving C++ language. As new language and library features were added in each C++ version, the limitations of the old front-end became apparent, leading to difficult-to-maintain code. Consequently, modern C++ programs were challenging to verify. To overcome this obstacle, we redeveloped the front-end, opting for a more robust approach using clang. The new front-end efficiently traverses the Abstract Syntax Tree (AST) in-memory using clang APIs and transforms each AST node into ESBMC's Intermediate Representation. Through extensive experimentation, our results demonstrate that ESBMC v7.3 with the new front-end significantly reduces parse and conversion errors, enabling successful verification of a wide range of C++ programs, thereby outperforming previous ESBMC versions. △ Less

Submitted 10 August, 2023; originally announced August 2023.

The structure of segregation in co-authorship networks and its impact on scientific production

Authors: Ana Maria Jaramillo, Hywel T. P. Williams, Nicola Perra, Ronaldo Menezes

Abstract: Co-authorship networks, where nodes represent authors and edges represent co-authorship relations, are key to understanding the production and diffusion of knowledge in academia. Social constructs, biases (implicit and explicit), and constraints (e.g. spatial, temporal) affect who works with whom and cause co-authorship networks to organise into tight communities with different levels of segregati… ▽ More Co-authorship networks, where nodes represent authors and edges represent co-authorship relations, are key to understanding the production and diffusion of knowledge in academia. Social constructs, biases (implicit and explicit), and constraints (e.g. spatial, temporal) affect who works with whom and cause co-authorship networks to organise into tight communities with different levels of segregation. We aim to look at aspects of the co-authorship network structure that lead to segregation and its impact on scientific production. We measure segregation using the Spectral Segregation Index (SSI) and find 4 ordered segregation categories: completely segregated, highly segregated, moderately segregated and non-segregated communities. We direct our attention to the non-segregated and highly segregated communities, quantifying and comparing their structural topologies and k-core positions. When considering communities of both categories (controlling for size), our results show no differences in density and clustering but substantial variability in core position. Larger non-segregated communities are more likely to occupy cores near the network nucleus, while the highly segregated ones tend to be closer to the network periphery. Finally, we analyse differences in citations gained by researchers within communities showing different segregation categories. Researchers in highly segregated communities get more citations from their community members in middle cores and gain more citations per publication in middle/periphery cores. Those in non-segregated communities get more citations per publication in the nucleus. To our knowledge, this work is the first to characterise community segregation in co-authorship networks and investigate the relationship between community segregation and author citations. △ Less

Submitted 3 May, 2023; v1 submitted 20 July, 2022; originally announced July 2022.

Comments: 13 pages, 5 figures

Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs

Authors: Fatimah K. Aljaafari, Rafael Menezes, Edoardo Manino, Fedor Shmarov, Mustafa A. Mustafa, Lucas C. Cordeiro

Abstract: Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially with the number of program threads and statements. We propose and evaluate EBF (Ensembles of Bounded Model Checking with Fuzzing) -- a technique that combines Bounded Model Checking (BMC) and Gray-Box Fuzzing (GBF) to find… ▽ More Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially with the number of program threads and statements. We propose and evaluate EBF (Ensembles of Bounded Model Checking with Fuzzing) -- a technique that combines Bounded Model Checking (BMC) and Gray-Box Fuzzing (GBF) to find software vulnerabilities in concurrent programs. Since there are no publicly-available GBF tools for concurrent code, we first propose OpenGBF -- a new open-source concurrency-aware gray-box fuzzer that explores different thread schedules by instrumenting the code under test with random delays. Then, we build an ensemble of a BMC tool and OpenGBF in the following way. On the one hand, when the BMC tool in the ensemble returns a counterexample, we use it as a seed for OpenGBF, thus increasing the likelihood of executing paths guarded by complex mathematical expressions. On the other hand, we aggregate the outcomes of the BMC and GBF tools in the ensemble using a decision matrix, thus improving the accuracy of EBF. We evaluate EBF against state-of-the-art pure BMC tools and show that it can generate up to 14.9% more correct verification witnesses than the corresponding BMC tools alone. Furthermore, we demonstrate the efficacy of OpenGBF, by showing that it can find 24.2% of the vulnerabilities in our evaluation suite, while non-concurrency-aware GBF tools can only find 0.55%. Finally, thanks to our concurrency-aware OpenGBF, EBF detects a data race in the open-source wolfMqtt library and reproduces known bugs in several other real-world programs, which demonstrates its effectiveness in finding vulnerabilities in real-world software. △ Less

Submitted 20 October, 2022; v1 submitted 13 June, 2022; originally announced June 2022.

ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation

Authors: Rafael Menezes, Daniel Moura, Helena Cavalcante, Rosiane de Freitas, Lucas C. Cordeiro

Abstract: In this work, we describe and evaluate the first model checker for verifying Kotlin programs through the Jimple intermediate representation. The verifier, named ESBMC-Jimple, is built on top of the Efficient SMT-based Context-Bounded Model Checker (ESBMC). It uses the Soot framework to obtain the Jimple IR, representing a simplified version of the Kotlin source code, containing a maximum of three… ▽ More In this work, we describe and evaluate the first model checker for verifying Kotlin programs through the Jimple intermediate representation. The verifier, named ESBMC-Jimple, is built on top of the Efficient SMT-based Context-Bounded Model Checker (ESBMC). It uses the Soot framework to obtain the Jimple IR, representing a simplified version of the Kotlin source code, containing a maximum of three operands per instruction. ESBMC-Jimple processes Kotlin source code together with a model of the standard Kotlin libraries and checks a set of safety properties. Experimental results show that ESBMC-Jimple can correctly verify a set of Kotlin benchmarks from the literature and that it is competitive with state-of-the-art Java bytecode verifiers. A demonstration is available at https://youtu.be/J6WhNfXvJNc. △ Less

Submitted 20 July, 2022; v1 submitted 9 June, 2022; originally announced June 2022.

Comments: ACM SIGSOFT International Symposium on Software Testing and Analysis 2022

COVID-19 is linked to changes in the time-space dimension of human mobility

Authors: Clodomir Santana, Federico Botta, Hugo Barbosa, Filippo Privitera, Ronaldo Menezes, Riccardo Di Clemente

Abstract: Socio-economic constructs and urban topology are crucial drivers of human mobility patterns. During the coronavirus disease 2019 pandemic, these patterns were reshaped in their components: the spatial dimension represented by the daily travelled distance, and the temporal dimension expressed as the synchronization time of commuting routines. Here, leveraging location-based data from de-identified… ▽ More Socio-economic constructs and urban topology are crucial drivers of human mobility patterns. During the coronavirus disease 2019 pandemic, these patterns were reshaped in their components: the spatial dimension represented by the daily travelled distance, and the temporal dimension expressed as the synchronization time of commuting routines. Here, leveraging location-based data from de-identified mobile phone users, we observed that, during lockdowns restrictions, the decrease of spatial mobility is interwoven with the emergence of asynchronous mobility dynamics. The lifting of restriction in urban mobility allowed a faster recovery of the spatial dimension compared with the temporal one. Moreover, the recovery in mobility was different depending on urbanization levels and economic stratification. In rural and low-income areas, the spatial mobility dimension suffered a more considerable disruption when compared with urbanized and high-income areas. In contrast, the temporal dimension was more affected in urbanized and high-income areas than in rural and low-income areas. △ Less

Submitted 27 July, 2023; v1 submitted 17 January, 2022; originally announced January 2022.

Comments: 29 pages, 14 figures. Peer-revied version: Santana, C., Botta, F., Barbosa, H. et al. COVID-19 is linked to changes in the time-space dimension of human mobility. Nat Hum Behav (2023)

Journal ref: Nature Human Behaviour, 7, 1729-1739 (2023)

Dynamic predictability and spatio-temporal contexts in human mobility

Authors: Bibandhan Poudyal, Diogo Pacheco, Marcos Oliveira, Zexun Chen, Hugo Barbosa, Ronaldo Menezes, Gourab Ghoshal

Abstract: Human travelling behaviours are markedly regular, to a large extent, predictable, and mostly driven by biological necessities (\eg slee**, eating) and social constructs (\eg school schedules, synchronisation of labour). Not surprisingly, such predictability is influenced by an array of factors ranging in scale from individual (\eg preference, choices) and social (\eg household, groups) all the w… ▽ More Human travelling behaviours are markedly regular, to a large extent, predictable, and mostly driven by biological necessities (\eg slee**, eating) and social constructs (\eg school schedules, synchronisation of labour). Not surprisingly, such predictability is influenced by an array of factors ranging in scale from individual (\eg preference, choices) and social (\eg household, groups) all the way to global scale (\eg mobility restrictions in a pandemic). In this work, we explore how spatio-temporal patterns in individual-level mobility, which we refer to as \emph{predictability states}, carry a large degree of information regarding the nature of the regularities in mobility. Our findings indicate the existence of contextual and activity signatures in predictability states, pointing towards the potential for more sophisticated, data-driven approaches to short-term, higher-order mobility predictions beyond frequentist/probabilistic methods. △ Less

Submitted 6 October, 2023; v1 submitted 4 January, 2022; originally announced January 2022.

Comments: 17 pages, 6 figures, 48 references

Estimating Active Cases of COVID-19

Authors: Javier Álvarez, Carlos Baquero, Elisa Cabana, Jaya Prakash Champati, Antonio Fernández Anta, Davide Frey, Augusto García-Agúndez, Chryssis Georgiou, Mathieu Goessens, Harold Hernández, Rosa Lillo, Raquel Menezes, Raúl Moreno, Nicolas Nicolaou, Oluwasegun Ojo, Antonio Ortega, Jesús Rufino, Efstathios Stavrakis, Govind Jeevan, Christin Glorioso

Abstract: Having accurate and timely data on confirmed active COVID-19 cases is challenging, since it depends on testing capacity and the availability of an appropriate infrastructure to perform tests and aggregate their results. In this paper, we propose methods to estimate the number of active cases of COVID-19 from the official data (of confirmed cases and fatalities) and from survey data. We show that t… ▽ More Having accurate and timely data on confirmed active COVID-19 cases is challenging, since it depends on testing capacity and the availability of an appropriate infrastructure to perform tests and aggregate their results. In this paper, we propose methods to estimate the number of active cases of COVID-19 from the official data (of confirmed cases and fatalities) and from survey data. We show that the latter is a viable option in countries with reduced testing capacity or suboptimal infrastructures. △ Less

Submitted 6 August, 2021; originally announced August 2021.

Comments: Presented at the 2nd KDD Workshop on Data-driven Humanitarian Map**: Harnessing Human-Machine Intelligence for High-Stake Public Policy and Resiliency Planning, August 15, 2021

Contrasting social and non-social sources of predictability in human mobility

Authors: Zexun Chen, Sean Kelty, Brooke Foucault Welles, James P. Bagrow, Ronaldo Menezes, Gourab Ghoshal

Abstract: Social structures influence a variety of human behaviors including mobility patterns, but the extent to which one individual's movements can predict another's remains an open question. Further, latent information about an individual's mobility can be present in the mobility patterns of both social and non-social ties, a distinction that has not yet been addressed. Here we develop a "colocation" ne… ▽ More Social structures influence a variety of human behaviors including mobility patterns, but the extent to which one individual's movements can predict another's remains an open question. Further, latent information about an individual's mobility can be present in the mobility patterns of both social and non-social ties, a distinction that has not yet been addressed. Here we develop a "colocation" network to distinguish the mobility patterns of an ego's social ties from those of non-social colocators, individuals not socially connected to the ego but who nevertheless arrive at a location at the same time as the ego. We apply entropy and predictability measures to analyse and bound the predictive information of an individual's mobility pattern and the flow of that information from their top social ties and from their non-social colocators. While social ties generically provide more information than non-social colocators, we find that significant information is present in the aggregation of non-social colocators: 3-7 colocators can provide as much predictive information as the top social tie, and colocators can replace up to 85% of the predictive information about an ego, compared with social ties that can replace up to 94% of the ego's predictability. The presence of predictive information among non-social colocators raises privacy concerns: given the increasing availability of real-time mobility traces from smartphones, individuals sharing data may be providing actionable information not just about their own movements but the movements of others whose data are absent, both known and unknown individuals. △ Less

Submitted 27 April, 2021; originally announced April 2021.

Comments: 20 pages, 6 figures

Finding Security Vulnerabilities in IoT Cryptographic Protocol and Concurrent Implementations

Authors: Fatimah Aljaafari, Rafael Menezes, Mustafa A. Mustafa, Lucas C. Cordeiro

Abstract: Internet of Things (IoT) consists of a large number of devices connected through a network, which exchange a high volume of data, thereby posing new security, privacy, and trust issues. One way to address these issues is ensuring data confidentiality using lightweight encryption algorithms for IoT protocols. However, the design and implementation of such protocols is an error-prone task; flaws in… ▽ More Internet of Things (IoT) consists of a large number of devices connected through a network, which exchange a high volume of data, thereby posing new security, privacy, and trust issues. One way to address these issues is ensuring data confidentiality using lightweight encryption algorithms for IoT protocols. However, the design and implementation of such protocols is an error-prone task; flaws in the implementation can lead to devastating security vulnerabilities. Here we propose a new verification approach named Encryption-BMC and Fuzzing (EBF), which combines Bounded Model Checking (BMC) and Fuzzing techniques to check for security vulnerabilities that arise from concurrent implementations of cyrptographic protocols, which include data race, thread leak, arithmetic overflow, and memory safety. EBF models IoT protocols as a client and server using POSIX threads, thereby simulating both entities' communication. It also employs static and dynamic verification to cover the system's state-space exhaustively. We evaluate EBF against three benchmarks. First, we use the concurrency benchmark from SV-COMP and show that it outperforms other state-of-the-art tools such as ESBMC, AFL, Lazy-CSeq, and TSAN with respect to bug finding. Second, we evaluate an open-source implementation called WolfMQTT. It is an MQTT client implementation that uses the WolfSSL library. We show that \tool detects a data race bug, which other approaches are unable to find. Third, to show the effectiveness of EBF, we replicate some known vulnerabilities in OpenSSL and CyaSSL (lately WolfSSL) libraries. EBF can detect the bugs in minimum time. △ Less

Submitted 27 April, 2021; v1 submitted 21 March, 2021; originally announced March 2021.

Differences in the spatial landscape of urban mobility: gender and socioeconomic perspectives

Authors: Mariana Macedo, Laura Lotero, Alessio Cardillo, Ronaldo Menezes, Hugo Barbosa

Abstract: Many of our routines and activities are linked to our ability to move; be it commuting to work, shop** for groceries, or meeting friends. Yet, factors that limit the individuals' ability to fully realise their mobility needs will ultimately affect the opportunities they can have access to (e.g., cultural activities, professional interactions). One important aspect frequently overlooked in human… ▽ More Many of our routines and activities are linked to our ability to move; be it commuting to work, shop** for groceries, or meeting friends. Yet, factors that limit the individuals' ability to fully realise their mobility needs will ultimately affect the opportunities they can have access to (e.g., cultural activities, professional interactions). One important aspect frequently overlooked in human mobility studies is how gender-centred issues can amplify other sources of mobility disadvantages (e.g., socioeconomic inequalities), unevenly affecting the pool of opportunities men and women have access to. In this work, we leverage on a combination of computational, statistical, and information-theoretical approaches to investigate the existence of systematic discrepancies in the mobility diversity (i.e., the diversity of travel destinations) of (1) men and women from different socioeconomic backgrounds, and (2) work and non-work travels. Our analysis is based on datasets containing multiple instances of large-scale, official, travel surveys carried out in three major metropolitan areas in South America: Medellín and Bogotá in Colombia, and São Paulo in Brazil. Our results indicate the presence of general discrepancies in the urban mobility diversities related to the gender and socioeconomic characteristics of the individuals. Lastly, this paper sheds new light on the possible origins of gender-level human mobility inequalities, contributing to the general understanding of disaggregated patterns in human mobility. △ Less

Submitted 2 March, 2022; v1 submitted 12 February, 2021; originally announced February 2021.

Comments: main + supplementary material. Final version accepted for publication

Journal ref: PLoS ONE 17, e0260874, 2022

Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors

Authors: Mohannad Aldughaim, Kaled Alshmrany, Rafael Menezes, Lucas Cordeiro, Alexandru Stancu

Abstract: Bounded model checking (BMC) is vital for finding program property violations. For unsafe programs, BMC can quickly find an execution path from an initial state to the violated state that refutes a given safety property. However, BMC techniques struggle to falsify programs that contain loops. BMC needs to incrementally unfold the program loops up to the bound $k$, exposing the property violation,… ▽ More Bounded model checking (BMC) is vital for finding program property violations. For unsafe programs, BMC can quickly find an execution path from an initial state to the violated state that refutes a given safety property. However, BMC techniques struggle to falsify programs that contain loops. BMC needs to incrementally unfold the program loops up to the bound $k$, exposing the property violation, which can thus lead to exploring a considerable state space. Here, we describe and evaluate the first verification method based on interval methods via contractors to reduce the domains of variables representing the search space. This reduction is based on the specified property modeled as functions representing the contractor constraints. In particular, we exploit interval methods via contractors to incrementally analyze the program loop variables and contract the domain where the property is guaranteed to hold to prune the search exploration, thus reducing resource consumption aggressively. Experimental results demonstrate the efficiency and efficacy of our proposed approach over a large set of benchmarks, including $7044$ verification tasks, compared with state-of-the-art BMC tools. Our proposed method can reduce memory usage up to $75$\% while verifying $1$\% more verification tasks. △ Less

Submitted 21 September, 2022; v1 submitted 21 December, 2020; originally announced December 2020.

FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs

Authors: Kaled M. Alshmrany, Rafael S. Menezes, Mikhail R. Gadelha, Lucas C. Cordeiro

Abstract: We describe and evaluate a novel white-box fuzzer for C programs named FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. FuSeBMC explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to p… ▽ More We describe and evaluate a novel white-box fuzzer for C programs named FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. FuSeBMC explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. FuSeBMC successfully participates in Test-Comp'21 and achieves first place in the Cover-Error category and second place in the Overall category. △ Less

Submitted 21 December, 2020; originally announced December 2020.

Comments: 4 pages

CAD2Real: Deep learning with domain randomization of CAD data for 3D pose estimation of electronic control unit housings

Authors: Simon Baeuerle, Jonas Barth, Elton Renato Tavares de Menezes, Andreas Steimer, Ralf Mikut

Abstract: Electronic control units (ECUs) are essential for many automobile components, e.g. engine, anti-lock braking system (ABS), steering and airbags. For some products, the 3D pose of each single ECU needs to be determined during series production. Deep learning approaches can not easily be applied to this problem, because labeled training data is not available in sufficient numbers. Thus, we train sta… ▽ More Electronic control units (ECUs) are essential for many automobile components, e.g. engine, anti-lock braking system (ABS), steering and airbags. For some products, the 3D pose of each single ECU needs to be determined during series production. Deep learning approaches can not easily be applied to this problem, because labeled training data is not available in sufficient numbers. Thus, we train state-of-the-art artificial neural networks (ANNs) on purely synthetic training data, which is automatically created from a single CAD file. By randomizing parameters during rendering of training images, we enable inference on RGB images of a real sample part. In contrast to classic image processing approaches, this data-driven approach poses only few requirements regarding the measurement setup and transfers to related use cases with little development effort. △ Less

Submitted 25 September, 2020; originally announced September 2020.

Comments: Proc. 30. Workshop Computational Intelligence, Berlin, 2020

ACM Class: I.2.10; I.4.8

CoronaSurveys: Using Surveys with Indirect Reporting to Estimate the Incidence and Evolution of Epidemics

Authors: Oluwasegun Ojo, Augusto García-Agundez, Benjamin Girault, Harold Hernández, Elisa Cabana, Amanda García-García, Payman Arabshahi, Carlos Baquero, Paolo Casari, Ednaldo José Ferreira, Davide Frey, Chryssis Georgiou, Mathieu Goessens, Anna Ishchenko, Ernesto Jiménez, Oleksiy Kebkal, Rosa Lillo, Raquel Menezes, Nicolas Nicolaou, Antonio Ortega, Paul Patras, Julian C Roberts, Efstathios Stavrakis, Yuichi Tanaka, Antonio Fernández Anta

Abstract: The world is suffering from a pandemic called COVID-19, caused by the SARS-CoV-2 virus. National governments have problems evaluating the reach of the epidemic, due to having limited resources and tests at their disposal. This problem is especially acute in low and middle-income countries (LMICs). Hence, any simple, cheap and flexible means of evaluating the incidence and evolution of the epidemic… ▽ More The world is suffering from a pandemic called COVID-19, caused by the SARS-CoV-2 virus. National governments have problems evaluating the reach of the epidemic, due to having limited resources and tests at their disposal. This problem is especially acute in low and middle-income countries (LMICs). Hence, any simple, cheap and flexible means of evaluating the incidence and evolution of the epidemic in a given country with a reasonable level of accuracy is useful. In this paper, we propose a technique based on (anonymous) surveys in which participants report on the health status of their contacts. This indirect reporting technique, known in the literature as network scale-up method, preserves the privacy of the participants and their contacts, and collects information from a larger fraction of the population (as compared to individual surveys). This technique has been deployed in the CoronaSurveys project, which has been collecting reports for the COVID-19 pandemic for more than two months. Results obtained by CoronaSurveys show the power and flexibility of the approach, suggesting that it could be an inexpensive and powerful tool for LMICs. △ Less

Submitted 26 June, 2020; v1 submitted 24 May, 2020; originally announced May 2020.

Comments: Presented at The KDD Workshop on Humanitarian Map**, San Diego, California USA, August 24, 2020

Network-Based Delineation of Health Service Areas: A Comparative Analysis of Community Detection Algorithms

Authors: Diego Pinheiro, Ryan Hartman, Erick Romero, Ronaldo Menezes, Martin Cadeiras

Abstract: A Health Service Area (HSA) is a group of geographic regions served by similar health care facilities. The delineation of HSAs plays a pivotal role in the characterization of health care services available in an area, enabling a better planning and regulation of health care services. Though Dartmouth HSAs have been the standard delineation for decades, previous work has recently shown an improved… ▽ More A Health Service Area (HSA) is a group of geographic regions served by similar health care facilities. The delineation of HSAs plays a pivotal role in the characterization of health care services available in an area, enabling a better planning and regulation of health care services. Though Dartmouth HSAs have been the standard delineation for decades, previous work has recently shown an improved HSA delineation using a network-based approach, in which HSAs are the communities extracted by the Louvain algorithm in hospital-patient discharge networks. Given the existent heterogeneity of communities extracted by different community detection algorithms, a comparative analysis of community detection algorithms for optimal HSA delineation is lacking. In this work, we compared HSA delineations produced by community detection algorithms using a large-scale dataset containing different types of hospital-patient discharges spanning a 7-year period in US. Our results replicated the heterogeneity among community detection algorithms found in previous works, the improved HSA delineation obtained by a network-based, and suggested that Infomap may be a more suitable community detection for HSA delineation since it finds a high number of HSAs with high localization index and a low network conductance. △ Less

Submitted 8 December, 2019; originally announced December 2019.

Gender Patterns of Human Mobility in Colombia: Reexamining Ravenstein's Laws of Migration

Authors: Mariana Macedo, Laura Lotero, Alessio Cardillo, Hugo Barbosa, Ronaldo Menezes

Abstract: Public stakeholders implement several policies and regulations to tackle gender gaps, fostering the change in the cultural constructs associated with gender. One way to quantify if such changes elicit gender equality is by studying mobility. In this work, we study the daily mobility patterns of women and men occurring in Medellín (Colombia) in two years: 2005 and 2017. Specifically, we focus on th… ▽ More Public stakeholders implement several policies and regulations to tackle gender gaps, fostering the change in the cultural constructs associated with gender. One way to quantify if such changes elicit gender equality is by studying mobility. In this work, we study the daily mobility patterns of women and men occurring in Medellín (Colombia) in two years: 2005 and 2017. Specifically, we focus on the spatiotemporal differences in the travels and find that purpose of travel and occupation characterise each gender differently. We show that women tend to make shorter trips, corroborating Ravenstein's Laws of Migration. Our results indicate that urban mobility in Colombia seems to behave in agreement with the "archetypal" case studied by Ravenstein. △ Less

Submitted 29 November, 2019; originally announced November 2019.

Comments: 12 pages, 6 figures. Comments are welcome

Journal ref: Proceedings of the conference "Complex Networks XI", pp. 269-281, Springer Proceedings in Complexity (2020)

Characterizing the Social Interactions in the Artificial Bee Colony Algorithm

Authors: Lydia Taw, Nishant Gurrapadi, Mariana Macedo, Marcos Oliveira, Diego Pinheiro, Carmelo Bastos-Filho, Ronaldo Menezes

Abstract: Computational swarm intelligence consists of multiple artificial simple agents exchanging information while exploring a search space. Despite a rich literature in the field, with works improving old approaches and proposing new ones, the mechanism by which complex behavior emerges in these systems is still not well understood. This literature gap hinders the researchers' ability to deal with known… ▽ More Computational swarm intelligence consists of multiple artificial simple agents exchanging information while exploring a search space. Despite a rich literature in the field, with works improving old approaches and proposing new ones, the mechanism by which complex behavior emerges in these systems is still not well understood. This literature gap hinders the researchers' ability to deal with known problems in swarms intelligence such as premature convergence, and the balance of coordination and diversity among agents. Recent advances in the literature, however, have proposed to study these systems via the network that emerges from the social interactions within the swarm (i.e., the interaction network). In our work, we propose a definition of the interaction network for the Artificial Bee Colony (ABC) algorithm. With our approach, we captured striking idiosyncrasies of the algorithm. We uncovered the different patterns of social interactions that emerge from each type of bee, revealing the importance of the bees variations throughout the iterations of the algorithm. We found that ABC exhibits a dynamic information flow through the use of different bees but lacks continuous coordination between the agents. △ Less

Submitted 8 April, 2019; originally announced April 2019.

Comments: 9 pages, 10 figures

Spatial concentration and temporal regularities in crime

Authors: Marcos Oliveira, Ronaldo Menezes

Abstract: Though crime is linked to different socio-economic factors, it exhibits remarkable regularities regardless of cities' particularities. In this chapter, we consider two fundamental regularities in crime regarding two essential aspects of criminal activity: time and space. For more than one century, we know that (1) crime occurs unevenly within a city and (2) crime peaks during specific times of the… ▽ More Though crime is linked to different socio-economic factors, it exhibits remarkable regularities regardless of cities' particularities. In this chapter, we consider two fundamental regularities in crime regarding two essential aspects of criminal activity: time and space. For more than one century, we know that (1) crime occurs unevenly within a city and (2) crime peaks during specific times of the year. Here we describe the tendency of crime to concentrate spatially and to exhibit temporal regularities. We examine these phenomena from the complex-system perspective of cities, accounting for the possibility of both spatial heterogeneity and non-stationarity in urban phenomena. △ Less

Submitted 11 January, 2019; originally announced January 2019.

Comments: 15 pages, 4 figures. To appear in "Understanding Crime through Science" (Springer, 2019)

Uncovering the Social Interaction in Swarm Intelligence with Network Science

Authors: Marcos Oliveira, Diego Pinheiro, Mariana Macedo, Carmelo Bastos-Filho, Ronaldo Menezes

Abstract: Swarm intelligence is the collective behavior emerging in systems with locally interacting components. Because of their self-organization capabilities, swarm-based systems show essential properties for handling real-world problems such as robustness, scalability, and flexibility. Yet, we do not know why swarm-based algorithms work well and neither we can compare the different approaches in the lit… ▽ More Swarm intelligence is the collective behavior emerging in systems with locally interacting components. Because of their self-organization capabilities, swarm-based systems show essential properties for handling real-world problems such as robustness, scalability, and flexibility. Yet, we do not know why swarm-based algorithms work well and neither we can compare the different approaches in the literature. The lack of a common framework capable of characterizing these several swarm-based algorithms, transcending their particularities, has led to a stream of publications inspired by different aspects of nature without a systematic comparison over existing approaches. Here, we address this gap by introducing a network-based framework---the interaction network---to examine computational swarm-based systems via the optics of the social dynamics of such interaction network; a clear example of network science being applied to bring further clarity to a complicated field within artificial intelligence. We discuss the social interactions of four well-known swarm-based algorithms and provide an in-depth case study of the Particle Swarm Optimization. The interaction network enables researchers to study swarm algorithms as systems, removing the algorithm particularities from the analyses while focusing on the structure of the social interactions. △ Less

Submitted 12 November, 2019; v1 submitted 8 November, 2018; originally announced November 2018.

Comments: 23 pages, 6 figures

Spatio-temporal variations in the urban rhythm: the travelling waves of crime

Authors: Marcos Oliveira, Eraldo Ribeiro, Carmelo Bastos-Filho, Ronaldo Menezes

Abstract: In the last decades, the notion that cities are in a state of equilibrium with a centralised organisation has given place to the viewpoint of cities in disequilibrium and organised from bottom to up. In this perspective, cities are evolving systems that exhibit emergent phenomena built from local decisions. While urban evolution promotes the emergence of positive social phenomena such as the forma… ▽ More In the last decades, the notion that cities are in a state of equilibrium with a centralised organisation has given place to the viewpoint of cities in disequilibrium and organised from bottom to up. In this perspective, cities are evolving systems that exhibit emergent phenomena built from local decisions. While urban evolution promotes the emergence of positive social phenomena such as the formation of innovation hubs and the increase in cultural diversity, it also yields negative phenomena such as increases in criminal activity. Yet, we are still far from understanding the driving mechanisms of these phenomena. In particular, approaches to analyse urban phenomena are limited in scope by neglecting both temporal non-stationarity and spatial heterogeneity. In the case of criminal activity, we know for more than one century that crime peaks during specific times of the year, but the literature still fails to characterise the mobility of crime. Here we develop an approach to describe the spatial, temporal, and periodic variations in urban quantities. With crime data from 12 cities, we characterise how the periodicity of crime varies spatially across the city over time. We confirm one-year criminal cycles and show that this periodicity occurs unevenly across the city. These `waves of crime' keep travelling across the city: while cities have a stable number of regions with a circannual period, the regions exhibit non-stationary series. Our findings support the concept of cities in a constant change, influencing urban phenomena---in agreement with the notion of cities not in equilibrium. △ Less

Submitted 2 November, 2018; v1 submitted 9 July, 2018; originally announced July 2018.

Comments: 11 pages, 4 figures

Journal ref: EPJ Data Science 2018 7:29

The Effect of Recency to Human Mobility

Authors: Hugo Barbosa, Fernando Buarque de Lima Neto, Alexandre Evsukoff, Ronaldo Menezes

Abstract: In recent years, we have seen scientists attempt to model and explain human dynamics and, in particular, human movement. Many aspects of our complex life are affected by human movements such as disease spread and epidemics modeling, city planning, wireless network development, and disaster relief, to name a few. Given the myriad of applications it is clear that a complete understanding of how peop… ▽ More In recent years, we have seen scientists attempt to model and explain human dynamics and, in particular, human movement. Many aspects of our complex life are affected by human movements such as disease spread and epidemics modeling, city planning, wireless network development, and disaster relief, to name a few. Given the myriad of applications it is clear that a complete understanding of how people move in space can lead to huge benefits to our society. In most of the recent works, scientists have focused on the idea that people movements are biased towards frequently-visited locations. According to them, human movement is based on an exploration/exploitation dichotomy in which individuals choose new locations (exploration) or return to frequently-visited locations (exploitation). In this work, we focus on the concept of recency. We propose a model in which exploitation in human movement also considers recently-visited locations and not solely frequently-visited locations. We test our hypothesis against different empirical data of human mobility and show that our proposed model is able to better explain the human trajectories in these datasets. △ Less

Submitted 25 June, 2015; v1 submitted 6 April, 2015; originally announced April 2015.

New generation of mobile phone viruses and corresponding countermeasures

Authors: Pu Wang, Marta C. González, Ronaldo Menezes, Albert-László Barabási

Abstract: The fast growing market for smart phones coupled with their almost continuous online presence makes these devices the new targets of virus writers. It has been recently found that the topological spread of MMS (Multimedia Message Services) viruses is highly restricted by the underlying fragmentation of the call graph. In this paper, we study MMS viruses under another type of spreading behavior: sc… ▽ More The fast growing market for smart phones coupled with their almost continuous online presence makes these devices the new targets of virus writers. It has been recently found that the topological spread of MMS (Multimedia Message Services) viruses is highly restricted by the underlying fragmentation of the call graph. In this paper, we study MMS viruses under another type of spreading behavior: scanning. We find that hybrid MMS viruses including some level of scanning are more dangerous to the mobile community than their standard topological counterparts. However, the effectiveness of both scanning and topological behaviors in MMS viruses can generally be limited by two controlling methods: (i) decreasing susceptible handsets' market share (OS it runs) and (ii) improving monitoring capacity to limit the frequency in which MMS messages can be sent by the mobile viruses. △ Less

Submitted 14 December, 2010; originally announced December 2010.

Comments: 19 pages, 6 figures