Abstract
Abstract This paper assesses Brazil's real convergence (1822–2019) through unit root tests and Markov Regime-Switching (MS) models in three different scenarios: towards (i) other six Latin American countries (LA6); (ii) Portugal; and (iii) the technological frontier country, the US. The extended unit root test results favour Brazil's very long-run real convergence towards LA6 and Portugal, but not the US. The estimated MS models, involving two different regimes, real convergence and real non-convergence/divergence, capture institutional quality's positive effect in promoting Brazil's real convergence.

Abstract
Zero-shot learning enables the recognition of classes not seen during training through the use of semantic information comprising a visual description of the class either in textual or attribute form. Despite the advances in the performance of zero-shot learning methods, most of the works do not explicitly exploit the correlation between the visual attributes of the image and their corresponding semantic attributes for learning discriminative visual features. In this paper, we introduce an attention-based strategy for deriving features from the image regions regarding the most prominent attributes of the image class. In particular, we train a Convolutional Neural Network (CNN) for image attribute prediction and use a gradient-weighted method for deriving the attention activation maps of the most salient image attributes. These maps are then incorporated into the feature extraction process of Zero-Shot Learning (ZSL) approaches for improving the discriminability of the features produced through the implicit inclusion of semantic information. For experimental validation, the performance of state-of-the-art ZSL methods was determined using features with and without the proposed attention model. Surprisingly, we discover that the proposed strategy degrades the performance of ZSL methods in classical ZSL datasets (AWA2), but it can significantly improve performance when using face datasets. Our experiments show that these results are a consequence of the interpretability of the dataset attributes, suggesting that existing ZSL datasets attributes are, in most cases, difficult to be identifiable in the image. Source code is available at https://github.com/CristianoPatricio/SGAM.

Abstract
Formal verification techniques aim at formally proving the correctness of a computer program with respect to a formal specification, but the expertise and effort required for applying formal specification and verification techniques and scalability issues have limited their practical application. In recent years, the tremendous progress with SAT and SMT solvers enabled the construction of a new generation of tools that promise to make formal verification more accessible for software engineers, by automating most if not all of the verification process. The Dafny system is a prominent example of that trend. However, little evidence exists yet about its accessibility. To help fill this gap, we conducted a set of 10 case studies of developing verified implementations in Dafny of some real-world algorithms and data structures, to determine its accessibility for software engineers. We found that, on average, the amount of code written for specification and verification purposes is of the same order of magnitude as the traditional code written for implementation and testing purposes (ratio of 1.14) – an “overhead” that certainly pays off for high-integrity software. The performance of the Dafny verifier was impressive, with 2.4 proof obligations generated per line of code written, and 24 ms spent per proof obligation generated and verified, on average. However, we also found that the manual work needed in writing auxiliary verification code may be significant and difficult to predict and master. Hence, further automation and systematization of verification tasks are possible directions for future advances in the field. © 2023, IFIP International Federation for Information Processing.

Abstract
The development of increasingly autonomous underwater vehicles has long been a research focus in underwater robotics. Recent advances in deep learning have shown promising results, offering the potential for fully autonomous behavior in underwater vehicles. However, its implementation requires improvements to the current vehicles. This paper proposes an onboard data processing framework for Deep Learning implementation. The proposed framework aims to increase the autonomy of the vehicles by allowing them to interact with their environment in real time, enabling real-time detection, control, and navigation.

Abstract
Os produtores da agricultura familiar são considerados uma classe específica no sistema social, visto que reúnem características das duas outras classes sociais, assim, ao mesmo tempo em que atuam como donos dos meios de produção também são trabalhadores. Nesse sentido o sistema de criação deve evitar erros de manejo sanitário para possibilitar uma maximização do lucro para os produtores. Dentre os erros mais comuns estão os que possibilitam as doenças parasitárias constituindo um dos principais entraves quando o manejo é inadequado. Portanto, o objetivo deste trabalho foi identificar a influência das doenças parasitárias na produção de subsistência do pequeno produtor da agricultura familiar. Foram visitadas 30 propriedades rurais escolhidas aleatoriamente na região Oeste Potiguar da zona rural do município de Mossoró, onde foi realizado um diagnóstico parasitário de endoparasitos (contagem de ovos por grama e larvas) e ectoparasitos. De acordo com o local e diagnóstico parasitários foram identificados ovos de Strongyloidea em 100% (30/30) das propriedades, Moniezia 23,3% (7/30) e oocistos de Eimeria 73,3% (22/30). As larvas identificadas por propriedade foram Haemonchus spp 90% (27/30), Trichostrongylus spp 86,6% (26/30), Oesophagostomum spp 20% (6/30) e Trichuris spp 3,3% (1/30). Quanto aos ectoparasitos foram identificados por locais de coleta em Damalinia caprae 46,6% (14/30) e Rhipicephalus microplus 10% (3/30). Concluindo que os produtores pesquisados apresentam criação de rebanhos caprinos com erros de manejo sanitário, ocasionando a presença de ecto e endoparasitos que podem influenciar nos baixos lucros associado a elevados gastos.

Abstract