Abstract
This research aims to analyze the positioning theory and discourse within Sao Paulo's Place Branding from 2014 to 2019, investigating the symbolic representations employed by the Sao Paulo Tourism Bureau to emphasize its branding endeavors. The methodology employed a framework based on Semprini's [10] Project/Manifestation approach and Discourse Analysis. The impetus behind this study arises from the substantial investments made by cities to craft comprehensive disclosure strategies and establish place branding for their respective regions. We observed aspects of Communication and DigitalMarketing in the three promotional videos produced by SPTuris in 2014, 2017, and 2019, which underwent meticulous analysis. Our findings unveiled a consistent thematic discourse despite shifts in political administration. The 2014 video accentuated multiculturalism and cosmopolitanism, while the 2017 edition highlighted experiential marketing, business, consumption, and cosmopolitan elements. Remarkably, the 2019 presentation featured images emphasizing receptivity. Themes such as Culture, Arts, and Gastronomy were recurrent across all videos. The scrutinized discourse reaffirms Sao Paulo's capital as a trendsetter within Brazil.

Abstract
Predictive Maintenance applications are increasingly complex, with interactions between many components. Black -box models are popular approaches based on deep -learning techniques due to their predictive accuracy. This paper proposes a neural -symbolic architecture that uses an online rule -learning algorithm to explain when the black -box model predicts failures. The proposed system solves two problems in parallel: (i) anomaly detection and (ii) explanation of the anomaly. For the first problem, we use an unsupervised state-of-the-art autoencoder. For the second problem, we train a rule learning system that learns a mapping from the input features to the autoencoder's reconstruction error. Both systems run online and in parallel. The autoencoder signals an alarm for the examples with a reconstruction error that exceeds a threshold. The causes of the signal alarm are hard for humans to understand because they result from a non-linear combination of sensor data. The rule that triggers that example describes the relationship between the input features and the autoencoder's reconstruction error. The rule explains the failure signal by indicating which sensors contribute to the alarm and allowing the identification of the component involved in the failure. The system can present global explanations for the black box model and local explanations for why the black box model predicts a failure. We evaluate the proposed system in a real -world case study of Metro do Porto and provide explanations that illustrate its benefits.

Abstract
The global push for environmental sustainability is driving substantial changes in power systems, prompting extensive grid upgrades. Policies and initiatives worldwide aim to reduce CO2 emissions, with a focus on increasing reliance on Renewable Energy Sources (RESs) and electrifying transportation. However, the geographical variability and uncertainties of RESs directly impact power generation and distribution, necessitating adjustments in transmission system planning and operation. This paper presents a Transmission Expansion Planning (TEP) model using the 2021 Texas snowstorm as a benchmark scenario, incorporating wind and solar energy penetration while addressing associated uncertainties. Climate Change (CC) and Extreme Weather Events (EWE) are integrated into the set of scenarios aiming at evaluating the proposed method's effectiveness. Comparisons in extreme operative conditions highlight the importance of network reliability and security, emphasizing the significance of merged grids. All simulations are conducted using the ACTIVSg2000 synthetic test system, which emulates the ERCOT grid, with comparisons made between TEP scenarios considering and disregarding CC and EWEs, supporting the concept of umbrella protection.

Abstract
Over the past two decades, Digital Transformation (DT) has been focused on improving businesses, industries, and the general public through significant breakthroughs. This paper examines the significant developments brought forth by DT and how they impact organizations. This analysis explores the impact of Virtual Reality (VR) and the Metaverse on global businesses, taking inspiration from successful case studies such as Netflix, Amazon, and Meta. This study emphasizes the potential of virtual reality and the Metaverse in facilitating remote meetings, training employees, engaging with consumers, and gathering data. Case studies and strategic recommendations are offered for overcoming barriers to the adoption of these digital technologies. The study finishes by addressing the future trajectory of DT and emphasizing the significance of devoting time, commitment, and resources to effectively utilize the range of potential offered by VR and the Metaverse. It highlights the importance for organizations to comprehend and handle this ever-changing environment to remain at the forefront of the digital frontier.

Abstract

Abstract
This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step. In this paper, we describe preliminary work on using LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, we attempt to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.