arXiv subjects

Rosiane de Freitas

Publications and source records attributed to Rosiane de Freitas.

12 recordsLinked to original sources

arXiv2026

Phase-Preserving Trimodal Transformer for Tropical Forest Biomass Estimation Using Optical and PolInSAR Data

The accurate estimation of Above-Ground Biomass (AGB) in mature tropical forests remains a critical challenge in remote sensing, primarily due to the saturation of Synthetic Aperture Radar (SAR) signals in high-density areas and persistent cloud cover affecting optical imagery. To overcome these physical limitations, we propose the Trimodal Coherent Co-attention Transformer (TCCT), a physics-informed deep learning architecture. The TCCT natively fuses optical surface reflectance (Landsat-5) with complex-valued Polarimetric SAR Interferometry (PolInSAR) data from both P and L bands. Unlike traditional fusion methods, our architecture employs complex-valued encoders to preserve spatial phase coherence, coupled with a dynamic co-attention mechanism that acts as an adaptive gating module, reducing the weight of cloud-corrupted optical pixels and shifting reliance to microwave phase data. We also derived a localized spatial allometric calibration model via Levenberg-Marquardt optimization, tailored to the specific wood density of the Paracou region in the Amazon basin. Evaluated using a two-stage protocol, the TCCT first underwent a rigorous 5-fold cross-validation to establish robust global weights (achieving a global RMSE of 4.19 m). Subsequently, following a localized spatial fine-tuning phase over 200 epochs, the model attained an absolute RMSE of 3.78 m and an $R^2$ of 0.33 for Canopy Height Models (CHM), outperforming standard Random Forest, CNN, and Vision Transformer baselines. Our ablation study confirms that preserving phase coherence mitigates deep-canopy signal saturation. When converted to AGB, the fine-tuned TCCT map yielded a Relative RMSE (rRMSE) of 4.51% in dense forest areas above 50 Mg/ha. By meeting the European Space Agency (ESA) BIOMASS mission requirement of less than 20% error, the TCCT provides a robust framework for continuous carbon stock mapping in tropical biomes.

cs.LG↗

arXiv2026

Retroactive Monotonic Priority Queues via Range Searching

The best-known fully retroactive priority queue costs $O(\log^2 m \log \log m)$ time per operation and uses $O(m \log m)$ space, where $m$ is the number of operations performed on the data structure. In contrast, standard (non-retroactive) priority queues can cost $O(\log m)$ time per operation and use $O(m)$ space. So far, it remains open whether these bounds can be achieved for fully retroactive priority queues. In this work, we study a restricted variant of priority queues known as monotonic priority queues. First, we show that finding the minimum in a retroactive monotonic priority queue is a special case of the range-searching problem. Then, we design a fully retroactive monotonic priority queue that costs $O(\log m)$ time per operation and uses $O(m)$ space, achieving the same bounds as a standard priority queue.

cs.DS↗

arXiv2026

Implementation and Brief Experimental Analysis of the Duan et al. (2025) Algorithm for Single-Source Shortest Paths

We present an implementation and experimental analysis of the deterministic algorithm proposed by Duan et al. (2025) for the Single-Source Shortest Path (SSSP) problem, which achieves the best-known asymptotic upper bound of $O(m \log^{2/3} n)$. We provide a worst-case C++ implementation of this algorithm utilizing $O(n \log^{1/3} n)$ space, as well as a variant that reduces memory usage to $O(n)$ while maintaining the same time complexity in expectation. We compare these implementations against Dijkstra's algorithm on sparse random graphs, grids, and U.S. road networks with up to 10 million vertices. Our results show that while the implementations adhere to their theoretical complexity bounds, large constant factors hinder their practical utility; Dijkstra's algorithm remains 3 to 4 times faster in all tested scenarios. Furthermore, we estimate that the number of vertices would need to vastly exceed $10^{67}$ for the worst-case implementation to outperform Dijkstra's. These findings suggest that a substantial reduction in constant factors is required before this theoretical breakthrough can displace established methods in practical applications.

cs.DS↗

arXiv2025

Domain Wall Control of Topological Qubits in the Kitaev SSH Chain

Zero energy states in one dimensional SSH Kitaev hybrid systems have emerged as promising candidates for topological qubits. In our work, we show that introducing a domain wall into a chain with anisotropic superconducting correlations provides a powerful way to control both the number and the nature of these boundary modes. The defect acts as a digital knob: its presence or absence flips the parity of zero modes and thus decides whether an isolated Majorana exists at the chain ends. This on/off mechanism is significantly more robust and simpler than fine-tuning global parameters such as chemical potential or hopping amplitudes. Moreover, anisotropy provides an additional lever to calibrate the effect of the defect, opening a pathway to architectures where topological qubits can be locally addressed by domain walls. This proposal reframes defects not as imperfections, but as useful resources for quantum information and computation.

cond-mat.mes-hall↗

arXiv2025

Generative transformations and patterns in LLM-native approaches for software verification and falsification

The emergence of prompting as the dominant paradigm for leveraging Large Language Models (LLMs) has led to a proliferation of LLM-native software, where application behavior arises from complex, stochastic data transformations. However, the engineering of such systems remains largely exploratory and ad-hoc, hampered by the absence of conceptual frameworks, ex-ante methodologies, design guidelines, and specialized benchmarks. We argue that a foundational step towards a more disciplined engineering practice is a systematic understanding of the core functional units--generative transformations--and their compositional patterns within LLM-native applications. Focusing on the rich domain of software verification and falsification, we conduct a secondary study of over 100 research proposals to address this gap. We first present a fine-grained taxonomy of generative transformations, abstracting prompt-based interactions into conceptual signatures. This taxonomy serves as a scaffolding to identify recurrent transformation relationship patterns--analogous to software design patterns--that characterize solution approaches in the literature. Our analysis not only validates the utility of the taxonomy but also surfaces strategic gaps and cross-dimensional relationships, offering a structured foundation for future research in modular and compositional LLM application design, benchmarking, and the development of reliable LLM-native systems.

cs.SE↗

arXiv2025

Improving polynomial bounds for the Graphical Traveling Salesman Problem with release dates on paths

The Graphical Traveling Salesman Problem with release dates (GTSP-rd) is a variation of the TSP-rd where each vertex in a weighted graph $G$ must be visited at least once, respecting the release date restriction. The edges may be traversed multiple times if necessary, as in some sparse graphs. This paper focuses on solving the GTSP-rd in paths. We consider two objective functions: minimizing the route completion time (GTSP-rd (time)) and minimizing the total distance traveled (GTSP-rd (distance)). We present improvements to existing dynamic programming algorithms, offering an $O(n)$ solution for paths where the depot is located at the extremity and an $O(n^2)$ solution for paths where the depot is located anywhere. For the GTSP-rd (distance), we propose an $O(n \log \log n)$ solution for the case with the depot at the extremity and an $O(n^2 \log \log n)$ solution for the general case.

cs.DS↗

arXiv2024

Exploring Monotone Priority Queues for Dijkstra Optimization

This paper presents a comprehensive overview of monotone priority queues, focusing on their evolution and application in shortest path algorithms. Monotone priority queues are characterized by the property that their minimum key does not decrease over time, making them particularly effective for label-setting algorithms like Dijkstra's. Some key data structures within this category are explored, emphasizing those derived directly from Dial's algorithm, including variations of multi-level bucket structures and radix heaps. Theoretical complexities and practical considerations of these structures are discussed, with insights into their development and refinement provided through a historical timeline.

cs.DS↗

arXiv2024

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

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.

cs.SE↗

arXiv2022

ESBMC-Jimple: Verifying Kotlin Programs via Jimple Intermediate Representation

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.

cs.SE↗

arXiv2022

Empirical Evaluation of Project Scheduling Algorithms for Maximization of the Net Present Value

This paper presents an empirical performance analysis of three project scheduling algorithms dealing with maximizing projects' net present value with unrestricted resources. The selected algorithms, being the most recently cited in the literature, are: Recursive Search (RS), Steepest Ascent Approach (SAA) and Hybrid Search (HS). The main motivation for this research is the lack of knowledge about the computational complexities of the RS, SAA, and HS algorithms, since all studies to date show some gaps in the analysis. Furthermore, the empirical analysis performed to date does not consider the fact that one algorithm (HS) uses a dual search strategy, which markedly improved the algorithm's performance, while the others don't. In order to obtain a fair performance comparison, we implemented the dual search strategy into the other two algorithms (RS and SAA), and the new algorithms were called Recursive Search Forward-Backward (RSFB) and Steepest Ascent Approach Forward-Backward (SAAFB). The algorithms RSFB, SAAFB, and HS were submitted to a factorial experiment with three different project network sampling characteristics. The results were analyzed using the Generalized Linear Models (GLM) statistical modeling technique that showed: a) the general computational costs of RSFB, SAAFB, and HS; b) the costs of restarting the search in the spanning tree as part of the total cost of the algorithms; c) and statistically significant differences between the distributions of the algorithms' results.

cs.AI↗

arXiv2018

Choosability in bounded sequential list coloring

The list coloring problem is a variation of the classical vertex coloring problem, extensively studied in recent years, where each vertex has a restricted list of allowed colors, and having some variations as the $(γ,μ)$-coloring, where the color lists have sequential values with known lower and upper bounds. This work discusses the choosability property, that consists in determining the least number $k$ for which it has a proper list coloring no matter how one assigns a list of $k$ colors to each vertex. This is a $Π_2^P$-complete problem, however, we show that $k$-$(γ,μ)$-choosability is an $NP$-problem due to its relation with the $k$-coloring of a graph and application of methods of proof in choosability for some classes of graphs, such as complete bipartite graph, which is $ 3 $-choosable, but $ 2 $-$(γ,μ)$-choosable.

cs.CC↗

arXiv2016

Distance geometry approach for special graph coloring problems

One of the most important combinatorial optimization problems is graph coloring. There are several variations of this problem involving additional constraints either on vertices or edges. They constitute models for real applications, such as channel assignment in mobile wireless networks. In this work, we consider some coloring problems involving distance constraints as weighted edges, modeling them as distance geometry problems. Thus, the vertices of the graph are considered as embedded on the real line and the coloring is treated as an assignment of positive integers to the vertices, while the distances correspond to line segments, where the goal is to find a feasible intersection of them. We formulate different such coloring problems and show feasibility conditions for some problems. We also propose implicit enumeration methods for some of the optimization problems based on branch-and-prune methods proposed for distance geometry problems in the literature. An empirical analysis was undertaken, considering equality and inequality constraints, uniform and arbitrary set of distances, and the performance of each variant of the method considering the handling and propagation of the set of distances involved.

cs.DS↗