Abstract ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the category of Test-Comp 2025.

This study conducts a comparative analysis of the performance of different programming languages on Android embedded systems, focusing on execution time. Through controlled experiments, we compared traditional and emerging programming languages (Java, Kotlin, C, C++, Python, Golang, and Rust) using a variety of representative algorithms. The results revealed significant disparities among the programming languages, with C and C++ performing significantly better than the others, although in some algorithms Golang approached close in terms of execution time. The native Android application languages, Java and Kotlin, showed intermediate results compared to the others, with very close outcomes between them. Python and Rust had the worst results, with Python's performance being justified by the interpreted nature of the language and the lack of multiprocessing features on Android. Rust was possibly hindered by its inability to efficiently access low-level resources when applied to the Android application layer.

The analysis of memory consumption is important for the stability and performance of Android applications. This work presents a method to extract and visualize memory-related data from Android bug report files, focusing on improving the debugging process for potential memory issues. The proposed method utilizes regular expressions for extracting key memory metrics and presents this data through interactive visualizations, aiding developers in identifying memory performance issues. We demonstrate the use of this visualization approach through an experimental analysis involving a high memory pressure scenario. This scenario allowed us to monitor memory consumption over time and analyze the causes of process terminations under this stress condition. Future work will involve evaluating the method's effectiveness under varying memory pressure scenarios, using the same or similar applications, and integrating advanced learning techniques for log analysis to capture complex patterns related to memory issues, ultimately helping to optimize system performance.

Abstract The cooperative verification of Bounded Model Checking and Fuzzing has proved to be one of the most effective techniques when testing C programs. FuSeBMC is a test-generation tool that employs BMC and Fuzzing to produce test cases. In Test-Comp 2023, we present an interval approach to FuSeBMC_IA, improving the test generator to use interval methods and abstract interpretation (via Frama-C) to strengthen our instrumentation and fuzzing. Here, an abstract interpretation engine instruments the program as follows. It analyzes different program branches, combines the conditions of each branch, and produces a Constraint Satisfaction Problem (CSP), which is solved using Constraint Programming (CP) by interval manipulation techniques called Contractor Programming. This process has a set of invariants for each branch, which are introduced back into the program as constraints. Experimental results show improvements in reducing CPU time (37%) and memory (13%), while retaining a high score.

Accordingly to Duchet (1987), the first paper of convexity on general graphs, in english, is the 1981 paper “Convexity in graphs”. One of its authors, Frank Harary, introduced in 1984 the first graph convexity games, focused on the geodesic convexity, which were investigated in a sequence of five papers that ended in 2003. In this paper, we continue this research line, extend these games to other graph convexities, and obtain winning strategies and complexity results. Among them, we obtain winning strategies for general convex geometries in graphs. We also obtain the first PSPACE-hardness results on convexity games, by proving that the normal play and the misère play of the hull game on the geodesic and the monophonic convexities are PSPACE-complete.

In this work, the Vehicle Routing Problem with Time Windows (VRPTW) is addressed as a way of incorporating dynamic characteristics of the urban express delivery logistics chain, exploring theoretical aspects that best define the problem and its instances. The problem is to determine minimum cost routes that must be performed by a fleet respecting the capacities of vehicles and the time windows associated with each delivery. A strategy that uses the Branch-Cut-and-Price method through the VRPsolver tool was applied to two sets of instances, the first being Solomon’s artificial classical instances and, the second, real instances of Brazilian urban cities adapted from the loggiBUD benchmark.

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; it is competitive with state-of-the-art Java bytecode verifiers. A demonstration is available at https://youtu.be/J6WhNfXvJNc.

Several systems proposed for processing keyword queries over relational databases rely on the generation and evaluation of Candidate Networks (CNs), i.e., networks of joined database relations that when processed as SQL queries, provide a relevant answer to the input keyword query. Although the evaluation of CNs has been extensively addressed in the literature, the problem of generating CNs efficiently and effectively has received much less attention. This challenging problem consists of automatically locating relations in the database that may contain relevant pieces of information, given a handful of keywords, and determining suitable ways of joining these relations to satisfy the implicit information needs expressed by a user while formulating his/her query. In this paper, we propose a novel approach for generating CNs, wherein the possible matches for the query in the database are efficiently enumerated at first. Thesequery matchesare then used to guide the CN generation process, avoiding the exhaustive search procedure used by the current state-of-art approaches. We show that our approach allows the generation of a compact set of CNs that leads to superior quality answers, and demands less resources in terms of processing time and memory. These claims are supported by a comprehensive set of experiments that we carried out using several query sets and datasets used in previous related works and whose results we report and analyze here.

The Gangal-Ranade algorithm presents the best approximation ratio for the classic scheduling problem with unit execution time and precedence constrained jobs, on a variable number of identical parallel machines, to minimize the makespan. This work presents results about the optimality of the algorithm when the acyclic directed graph (DAG) that represents the precedence constraints are arborescences (directed trees, in-tree and out-tree), reinforcing that these types of DAGs provide optimal substructures for the problem. Understanding the behavior of this algorithm for classes of arborescences can lead to optimality or better approximations for classes of larger DAGs, which is our ongoing research work. Furthermore, the search for optimal cases for algorithms such as Gangal-Ranade can provide intuition to obtain partial answers to problems that remain open, such as the famous Open 8 in the list presented in the classical Garey and Johnson book.

A fast way to reconstruct the three-dimensional molecular conformation of SARS-CoV-2 virus proteins is addressed in this article, involving the most worrying variant discovered in patients from Brazil, the lineage$B$.1.1.28/$P$.1. The proposed methodology is based on the sequencing of virus proteins and that, through the incorporation of mutations in silico, which are then computationally reconstructed using an enumerative feasibility algorithm validated by the Ramachandran diagram and structural alignment, in addition to the subsequent study of structural stability through classical molecular dynamics. From the resulting structure to the ACE2-RBD complex, the valid solution presented 97.06% of the residues in the most favorable region while the reference crystallographic structure presented 95.0%, a difference therefore very small and revealing the great consistency of the developed algorithm. Another important result was the low RMSD alignment between the best solution by the BP algorithm and the reference structure, where we obtained 0.483Å. Finally, the molecular dynamics indicated greater structural stability in the ACE2-RBD interaction with the P.1 strain, which could be a plausible explanation for convergent evolution that provides an increase in the interaction affinity with the ACE2 receptor.

In this work, an initial study on the automatic recognition of the main Brazilian music genres is presented: Axé, Forró, MPB, Rock, Samba, and Sertanejo. Through the extraction of representative musical characteristics, automatic classification experiments were performed applying classical supervised learning algorithms and Weka ML tool. An analysis of the main available databases was also carried out: GTZAN, FMA, AudioSet, RWC, ISMIR, Magnatune, and LMD. There is a scarcity of cultural diversity on these bases, most of which concentrate globally more popular styles such as Pop and Rock, reinforcing the need to include more diverse and culturally identifiable genres, such as Brazilians. The preliminary results obtained demonstrate the adequacy of the recognition process of the main Brazilian musical genres.

Using mobile devices is part of modern daily life for communication, work, and leisure. Its use in entertainment events such as music concert and sports games is easily noted. Thus, in this work, we investigate how these devices can increase engagement in entertainment events. For this, we developed a collaborative game called Cabo DIGuerra that uses motion and audio sensors in an interactive dynamic with the audience using concepts from Mobile Crowd Sensing and User eXperience. The game was evaluated through experimental studies both in a controlled environment and in real use scenarios of the application, highlighting its educational potential beyond entertainment.

The development of Computational Thinking has been pointed out by experts as fundamental in the lives of human beings. This article deals with the application of a game-based didactic sequence based on the fundamentals of Computer Science in a class of primary school children, to promote engagement in the development of mathematical activities and analyze the impact of the development of logical and algorithmic reasoning in the solution of mathematical problems in the classroom. The didactic sequence considered the cognitive development of the children as well as the personal evolution during the process. Preliminary results indicate that the didactic sequence had a positive impact on student learning, showing a rate of learning evolution of 18% in the test group and 5% in the control group.

This innovative practice full paper presents a set of engaging actions aimed to encourage women to pursue a Computer Science career in a city of a third world country (Manaus, Brazil). Despite worldwide efforts to promote gender equality, typically, women account for less than 30% of the workforce in technological areas. In third world countries, the situation is much more unbalanced. Poor educational and economic conditions, allied with a chauvinism culture contaminated by sexism and stereotypes, are strong forces that repel the young girls from IT areas. As a result, the percentage of women in local Computer Science majors is lower than expected. The authors detail a program to involve girls from all school levels in computer science career, which is indeed the adaptation of a national program, combined with indigenous elements. The mentioned adaptation was a key success factor to catch the attention of students and local educators. Some activities that are included in this program are lectures at scientific, technological and gender discussion events, realization of dynamics in schools for the dissemination of computational thinking in children and young students, training students to take part in programming contests and develop knowledge into real computational applications. These actions resulted in highlights achieved in programming contests and prizes obtained through application development, and have provided a more conducive academic environment to discuss issues related to the female gender in science and technology fields. Besides the fundamentals of the program, the authors present the results of the last three initiatives, which happened in conjunction with local events, and the promising opportunities perceived in Computer Science major of a local university.

Several systems for processing keyword queries over relational databases rely on the generation and evaluation of Candidate Networks (CNs), i.e., networks of joined relations that when processed as SQL queries, provide a relevant answer to the input keyword query. Although the evaluation of CNs has been extensively addressed in the literature, the problem of generating CNs has received much less attention. We propose a novel approach for generating CNs, wherein the possible matches for the query in the database are efficiently enumerated at first. These query matches are then used to guide the CN generation process, avoiding the exhaustive search procedure used by the current state-of-art approaches. We experimentally show that our approach allows the generation of a compact set of CNs that results in superior quality answers and demands less resources in terms of processing time and memory.

We present a strategy to improve an evolutionary process related to a hybridization of a genetic algorithm, strongly based on local search, for the weighted tardiness and Just-in-Time scheduling problems without idle time. The presented solutions represent a schedule in identical parallel machines that are indirectly encoded in a single sequence. An empirical analysis of these features is presented, by comparing this method with the previously one proposed, results from the literature, and also with an exact method, based on an IP formulation, for smaller instances, also proposed by the authors. With the proposed improvements, it was possible to solve larger instances up to 300 jobs and 2-20 parallel machines.

In this paper we present a correlation between a variation of the list problem coloring in graphs, the (γ, μ)-coloring, and the property of choosability in graphs, resulting in the k-(γ, μ)-choosability. The list coloring problem is a variation of the classical vertex coloring problem, introduced by Erdos et al. in 1979, along with a property very studied in list coloring: the choosability in graphs. In this work, algorithms were developed to determine the k-choosability and the k-(γ, μ)-choosability of a general simple graph, and a greedy heuristic based on DSATUR. In addition, we applied special techniques to prove the property of choosability in some classes of graphs, involving a general proof for simple graphs, which guarantees that if a graph is k-colorable it is also k-(γ, μ)-choosable, being the computational complexity reduced from the class Πp2-complete to the NP-complete.

The schema matching problem consists of finding semantic correspondences between elements (e.g., attributes) of two database schemas. Typically, methods to solve this problem first use pair-wise functions called matchers to generate similarity scores values between pairs of elements from the two schemas. These scores are used as estimations of the correspondence between elements. Next, matchers are combined to establish which pairs of elements must be mapped when integrating the two schemas. For this, the best-known schema matching methods rely on fixed heuristics. We consider that using fixed heuristics is not always helpful to cope with a variety of database and element mismatch cases and argue that machine learning (ML) techniques comprise suitable alternatives to properly combine matchers. In this paper we propose ALMa (Active Learning Matching), a novel method for combining matchers based on active learning, which is an interesting and effective machine learning technique that efficiently exploits the users' expertise on the matching task. We report the results of experiments we carried out comparing ALMa with COMA, a well-known schema matching method in the literature based on fixed heuristics, and with YAM, a recent schema matching method based on supervised learning. In the experiments, ALMa achieved results better or at least similar to the baselines, while demanded less user effort, confirming the suitability of using active learning for combining matchers.

This paper presents a framework to instantiate software technologies selection approaches by using search techniques. The software technologies selection problem (STSP) is modeled as a Combinatorial Optimization problem aiming attending different real scenarios in Software Engineering. The proposed framework works as a top-level layer over generic optimization frameworks that implement a high number of metaheuristics proposed in the technical literature, such as JMetal and OPT4J. It aims supporting software engineers that are not able to use optimization frameworks during a software project due to short deadlines and limited resources or skills. The framework was evaluated in a case study of a complex real-world software engineering scenario. This scenario was modeled as the STSP and some experiments were executed with different metaheuristics using the proposed framework. The results indicate its feasibility as support to the selection of software technologies.

The traditional way to identify malicious programs is to compare the code body with a set of previously stored code patterns, also known as signatures, extracted from already identified malware code. To nullify this identification process, the malware developers can insert in their creations the ability to modify the malware code when the next contamination process takes place, using obfuscation techniques. One way to deal with this metamorphic malware behavior is the use of dependency graphs, generated by surveying dependency relationships among code elements, creating a model that is resilient to code mutations. Analog to the signature model, a matching procedure that compares these graphs with a reference graph database is used to identify a malware code. Since graph matching is a NP-hard problem, it is necessary to find ways to optimize this process, so this identification technique can be applied. Using dependency graphs extracted from binary code, we present an approach to reduce the size of the reference dependency graphs stored on the graph database, by introducing a node differentiation based on its features. This way, in conjunction with the insertion of virtual paths, it is possible to build a virtual clique used to identify and dispose of less relevant elements of the original graph. The use of dependency graph reduction also produces more stable results in the matching process. To validate these statements, we present a methodology for generating these graphs from binary programs and compare the results achieved with and without the proposed approach in the identification of the Evol and Polip metamorphic malware.

The problem of estimating the full three-dimensional structure of a molecule, determining the position in space of all the atoms that compose it, is called Molecular Distance Geometry Problem (MDGP). To do this from an incomplete set of distances is NP-hard computational problem, where to get a feasible solution in a reasonable execution time presenting interesting mathematical and computational challenges. In this work, continuous and discrete mathematical approaches to solve MDGP is revised, based on the analysis of two types of calculating of sphere intersection: solving nonlinear systems from interatomic Euclidean distance equations, or solving internal coordinate systems using matrix multiplication techniques. We adapted the Branch-and-Prune (BP) method considering four spheres intersection. Computational experiments using instances from PDB benchmark are performed, determining the 3D structure based on our theoretical assumptions in a competitive computational processing time.

An adequate task allocation plan is an effective strategy to reduce collaboration issues in distributed software development. Practitioners adopt distinct processes to allocate tasks as well as diverse labels for the same activities and artifacts. This diversity is also found in literature. Task allocation proposals consider different elements and use distinct names for the same concepts. The lack of a standardized vocabulary and of an understanding of the elements involved impairs knowledge acquisition and sharing. Our paper presents a domain ontology to represent concepts related to task allocation in distributed teams. The ontology was defined based on a literature systematic mapping and on the opinion of experts. Preliminary evaluation suggests that the relationships among concepts are valid in real projects. The ontology brings awareness to managers regarding the factors related to task allocation planning and provides researchers with a framework to define processes and design tools to support such activity.

Distributed Software Development (DSD) emerged from the need to achieve geographically distant customers and currently, allows organizations have global customers and other benefits. This scenario has given rise to new Software Engineering challenges resulting from DSD particularities. Several Systematic Reviews were conducted to address these new challenges. The objective of this paper is to categorize systematic reviews conducted in DSD context. We used the systematic review method to identify SLRs (Systematic Literature Reviews) that address DSD aspects. This study is categorized as a tertiary review. Of fourteen SLRs, seven address aspects of managing distributed development. Four SLRs addressed topics of engineering process. The three remaining are related to Requirements, Design and Software Engineering Education in DSD. The topic areas covered by SLRs are limited, where the majority are focused on summarize the current knowledge concerning a research question. Despite the number of SLRs, the amount of empirical studies is relatively small.