Abstract
Over the last few years, the interest in the analysis of the energy consumption of Android applications has been increasing significantly. Indeed, there are a considerable number of studies which aim at analyzing the energy consumption in the Android ecosystem, such as measuring/estimating the energy consumed by an application or block of code, or even detecting energy expensive coding patterns or APIs. In this paper, we present an initial study of the impact of memoization in the energy consumption of Android applications. We compare implementations of 18 methods from different applications, with and without using memoization, and measure the energy consumption of both of them. The results show that using memoization can be a good approach for saving energy, since 13 of those methods decreased their energy consumption.

Abstract
Microgrids are often designed as energy systems that supply electrical and thermal loads with local resources such as combined heat and power units, renewable energy sources, diesel generators, and others. However, increasing interaction between natural gas and electrical systems, in addition to increased penetration of natural gas fired units gives rise to both opportunities and challenges in microgrid operation scheduling. In this paper, the energy hub concept is used to construct a scenario-based model for the optimal scheduling of electrical and thermal resources in a microgrid with integrated electrical and natural gas infrastructures. The objective function of the proposed model minimizes the expected operation costs while considering all network constraints and uncertainties. The natural gas and electricity flow equations are linearized and formulated as a mixed-integer linear programming problem. Scenarios associated with stochastic variables such as renewable generation and electrical and thermal loads are generated using the corresponding probability distribution functions and reduced using a scenario reduction technique. The proposed model is applied to an energy hub-based microgrid and the simulation results demonstrate the effectiveness of the approach. Furthermore, the benefits of implementing electrical and thermal demand response schemes are quantified. Also, more in-depth analyses for this network-constrained model are performed, including natural gas flow rate variations, natural gas pressures, power flow, and nodal voltages.

Abstract
This paper presents a minimal model of the functioning of program verification and property checking tools based on (i) the encoding of loops as non-iterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediate single-assignment (SA) form. The model captures the basic workflow of tools like Boogie, Why3, or CBMC, building on a clear distinction between operational and axiomatic semantics. This allows us to consider separately the soundness of program annotation, loop encoding, translation into SA form, and VC generation, as well as appropriate notions of completeness for each of these processes. To the best of our knowledge, this is the first formalization of a bounded model checking of software technique, including soundness and completeness proofs using Hoare logic; we also give the first completeness proof of a deductive verification technique based on a conservative encoding of invariant-annotated loops with assume/assert in SA form, as well as the first soundness proof based on a program logic.

Abstract
In this work we focus on the influence of salt water as the medium between two coupling coils to design a wireless power transfer system. An electrical circuit model and an adequate characterization approach is presented to account for the power losses in the conductive medium. Optimum values for the load and efficiency of the power link are determined. Experimental results are provided to compare the performance of the coupling coils between different coupling mediums (air, fresh and salt water).

Abstract
Machine Learning algorithms are often too complex to be studied from a purely analytical point of view. Alternatively, with a reasonably large number of datasets one can empirically observe the behavior of a given algorithm in different conditions and hypothesize some general characteristics. This knowledge about algorithms can be used to choose the most appropriate one given a new dataset. This very hard problem can be approached using metalearning. Unfortunately, the number of datasets available may not be sufficient to obtain reliable meta-knowledge. Additionally, datasets may change with time, by growing, shrinking and editing, due to natural actions like people buying in a e-commerce site. In this paper we propose dataset morphing as the basis of a novel methodology that can help overcome these drawbacks and can be used to better understand ML algorithms. It consists of manipulating real datasets through the iterative application of gradual transformations (morphing) and by observing the changes in the behavior of learning algorithms while relating these changes with changes in the meta features of the morphed datasets. Although dataset morphing can be envisaged in a much wider framework, we focus on one very specific instance: the study of collaborative filtering algorithms on binary data. Results show that the proposed approach is feasible and that it can be used to identify useful metafeatures to predict the best collaborative filtering algorithm for a given dataset.

Abstract