Abstract
As software becomes more complex and assumes an even greater role in our lives, formal verification is set to become the gold standard in securing software systems into the future, since it can guarantee the absence of errors and entire classes of attack. Recent advances in formal verification are being used to secure everything from unmanned drones to the internet. At the same time, the usable security research community has made huge progress in improving the usability of security products and end-users comprehension of security issues. However, there have been no human-centered studies focused on the impact of formal verification on the use and adoption of formally verified software products. We propose a research agenda to fill this gap and to contribute with the first collection of studies on people's mental models on formal verification and associated security and privacy guarantees and threats. The proposed research has the potential to increase the adoption of more secure products and it can be directly used by the security and formal methods communities to create more effective and secure software tools.

Abstract
This work addresses the use of hyperspectral imaging systems for remote detection of marine litter concentrations in oceanic environments. The work consisted on mounting an off-the-shelf hyperspectral imaging system (400-2500 nm) in two aerial platforms: manned and unmanned, and performing data acquisition to develop AI methods capable of detecting marine litter concentrations at the water surface. We performed the campaigns at Porto Pim Bay, Fail Island, Azores, resorting to artificial targets built using marine litter samples. During this work, we also developed a Convolutional Neural Network (CNN-3D), using spatial and spectral information to evaluate deep learning methods to detect marine litter in an automated manner. Results show over 84% overall accuracy (OA) in the detection and classification of the different types of marine litter samples present in the artificial targets.

Abstract
Traditional detection of aquatic invasive species, via morphological identification is often time-consuming and can require a high level of taxonomic expertise, leading to delayed mitigation responses. Environmental DNA (eDNA) detection approaches of multiple species using Illumina-based sequencing technology have been used to overcome these hindrances, but sample processing is often lengthy. More recently, portable nanopore sequencing technology has become available, which has the potential to make molecular detection of invasive species more widely accessible and to substantially decrease sample turnaround times. However, nanopore-sequenced reads have a much higher error rate than those produced by Illumina platforms, which has so far hindered the adoption of this technology. We provide a detailed laboratory protocol and bioinformatic tools to increase the reliability of nanopore sequencing to detect invasive species, and we test its application using invasive bivalves. We sampled water from sites with pre-existing bivalve occurrence and abundance data, and contrasting bivalve communities, in Italy and Portugal. We extracted, amplified and sequenced eDNA with a turnaround of 3.5 days. The majority of processed reads were = 99 % identical to reference sequences. There were no taxa detected other than those known to occur. The lack of detections of some species at some sites could be explained by their known low abundances. The approach is now being tested on other target taxa such as fish and other vertebrates.

Abstract
This study aims to identify and systematically compare the main large-scale agile frameworks that companies can adopt to manage the work of large-scale and distributed teams. Through this, companies can more consciously perform a better-informed decision on the choice of the framework that best fits the practices and challenges of their organizations. This work employs a qualitative approach supported by an exploratory analysis that identifies and explores the processes of migration to a large-scale agile. In the first phase, fifteen assessment criteria for scaling agile are discussed. In a second phase, these criteria are used to perform a comparative analysis of six large-scale agile frameworks (i.e., DAD, LeSS, Nexus, SAFe, Scrum at Scale, and Spotify). The findings reveal there isn't a dominant large-scale agile framework in all dimensions. However, it is possible to identify frameworks like Nexus and Spotify that target smaller teams and offer low technical complexity. These frameworks easily accommodate changes, while there are other frameworks like SAFe and DAD that offer high levels of scalability but require more demanding and deep efforts in changing work processes in an organization.

Abstract
This paper presents a conjectured-price-response equilibrium approach for modeling both centralized generation (CG) and behind-the-meter distributed generation (BMDG). A Nash game is set up with two constraints linking the CG and BMDG decisions to satisfy both the electricity demand in an energy market and the firm capacity in a capacity market. CG agents maximize their market profits while BMDG customers minimize their net supply costs, making decisions on their annual capacity investments and hourly productions decisions. Customers' costs account for 1) the energy bought from the grid minus the BMDG energy surpluses sold; 2) the payment of the grid access tariff (power and energy-based terms) and 3) the BMDG capacity investments' costs. The equilibrium conditions enable to represent different degrees of oligopoly using conjectural variations in both the energy and capacity markets. This work proves that such an equilibrium problem can be solved through an equivalent, yet simpler-to-solve, quadratic minimization problem. Some case examples compare the results of the proposed joint energy and capacity equilibrium with those from an energy-only equilibrium. Among other conclusions, these cases show that the proposed equilibrium sends adequate economic signals to the consumers to taper off the total system peak demand, whenever the weight of the power-based term of the access tariff is not extremely high.

Abstract
In recent years there has been a marked increase in bank fraud by SMS (Short Messaging System) and voice. One of the factors contributing to increase in cases of SMS fraud is the low cost of acquiring large volumes of messages, the reliability (the message will reach the recipient) and the fact that it does not need the Internet to reach the victim. In relation to financial fraud by voice, these can be used to persuade victims to make bank transfers to fraudulent accounts, with the promise of receiving large sums in prizes. The prevention of these types of fraud is not a trivial task, as it requires the application of appropriate techniques and methods depending on their nature. This article presents a Systematic Literature Review (SLR) from 2015 to 2020, with the aim of analyzing the state of the art on bank frauds committed by SMS or voice. The SLR allowed the identification of the most common types of bank fraud by SMS or voice, and the respective detection techniques.