Abstract
Advancements in the energy efficiency and computational power of embedded devices allow developers to equip resource-constrained systems with a greater number of features and more complex behavior. As complexity of a system grows, so does the difficulty in demonstrating its overall correctness. Formal methods have been successfully applied in a variety of verification and validation scenarios, but their wide adoption in the industry and academia is still lackluster. Among the explanations listed in the literature for the low adoption of these techniques are the perceived difficulty of getting into formal practices and how formal tools are not usually aimed at practical use cases. Striving to address these issues, we present MARS, an open-source domain-specific language for the safe instrumentation of runtime verification monitors into real-time resource-constrained distributed systems. Our main objective with MARS is to ease the integration of runtime verification monitors in distributed applications while also providing developers with evidence of their correct instrumentation in the context of systems where dependability and temporal requirements need to be respected even under extreme resource constraints. We present the language syntax, the set of tools embedded into its compiler, its functionalities, and a use case to exemplify its use in a practical distributed application.

Abstract
The footwear industry is energy-intensive and, consequently, a source of large amounts of greenhouse gas emissions every year. Issues related to climate change and growing conflicts on a global scale that impact the prices of raw materials and energy prices have led companies in the footwear industry to take actions to mitigate these impacts. Among these actions is the growing focus on producing its energy from energy systems based on renewable sources and battery energy storage units. This paper addresses the energy-efficient manufacturing scheduling in footwear industries with onsite energy production from a photovoltaic system with batteries. The problem is formulated as a mixed integer linear programming problem. Different objectives are presented, depending on the priorities of the entity that owns the footwear factory, namely, minimizing operation costs, minimizing CO2 emissions, or both. The case study is footwear factory located in Portugal that uses a manufacturing process based on injection molding. The results show the effectiveness of the proposed approach, with active demand side management playing a fundamental role in shifting periods of higher energy consumption to periods of lower prices or lower CO2 emissions. Also, Pareto fronts are depicted to make the trade-off between CO2 emissions and operation costs. As expected, the reduction of CO2 emissions promotes an increase on operation costs. Furthermore, a sensitivity analysis is carried out on the increase in photovoltaic capacity and battery capacity. The results show that increasing photovoltaic and battery capacity promotes reductions in costs up to 30% and in the emissions up to 37%.

Abstract
This study focuses on the assessment of ground vibrations due to pile driving activities. Given the likelihood of excessive vibration due to the driving process, it is imperative to predict vibration levels during the design phase. The primary goal of this work is to integrate machine learning techniques, specifically Extreme Gradient Boosting (XGBoost) and Artificial Neural Networks (ANNs) for real-time vibration prediction. The training dataset was generated using a validated numerical model and the trained models were validated based on experimental results. This validation process highlights the efficiency and accuracy of Extreme Gradient Boosting in predicting the-free-field response of the ground.

Abstract
Tabulation is a well-known technique for improving the efficiency of recursive functions with redundant function calls. A key point in the application of this technique is to identify a suitable representation for the table. In this paper, we propose the use of zippers as tables in the tabulation process. Our approach relies on a generic function zipWithZipper, that makes strong use of lazy evaluation to traverse two zippers in a circular manner. The technique turns out to be particularly efficient when the arguments to recursive calls are closely situated within the function domain. For example, in the case of natural numbers this means function calls on fairly contiguous values. Likewise, when dealing with tree structures, it means functions calls on immediate sub-trees and parent nodes. This results in a concise and efficient zipper-based embedding of attribute grammars.

Abstract
A presente obra, “O Habitar de Ensinar e do Aprender OnLIFE em Tempos de Ecologias Inteligentes”, dá continuidade às discussões sobre o Habitar do Ensinar e do Aprender realizadas nas obras anteriores a saber: “O Habitar do Ensinar e do Aprender OnLIFE: Vivências na Educação Contemporânea” (2021); “O Habitar do Ensinar e do Aprender: Desafios para/na/da Educação OnLIFE” (2022); e “O Habitar do Ensinar e do Aprender: as diferentes dimensões da/na Educação OnLIFE” (2023). Assim, embora publicada no ano de 2024, a obra está intrinsecamente ligada à produção do IV RIEOnLIFE e do VIII WLC em 2023, que ocorreram no Instituto Federal do Norte de Minas Gerais (IFNMG). Para tanto, damos continuidade às discussões sobre o Habitar do Ensinar e do Aprender OnLIFE, o qual se desenvolve num tempo constituído por inteligências diversas (humanas e não humanas), que conectadas formam o que denominamos de “ecologias inteligentes”.

Abstract