Hybridizing Deep Learning and Neuroevolution: Application to the Spanish Short-Term Electric Energy Consumption Forecasting

The electric energy production would be much more efficient if accurate estimations of the future demand were available, since these would allow allocating only the resources needed for the production of the right amount of energy required. With this motivation in mind, we propose a strategy, based on neuroevolution, that can be used to this aim. Our proposal uses a genetic algorithm in order to find a sub-optimal set of hyper-parameters for configuring a deep neural network, which can then be used for obtaining the forecasting. Such a strategy is justified by the observation that the performances achieved by deep neural networks are strongly dependent on the right setting of the hyper-parameters, and genetic algorithms have shown excellent search capabilities in huge search spaces. Moreover, we base our proposal on a distributed computing platform, which allows its use on a large time-series. In order to assess the performances of our approach, we have applied it to a large dataset, related to the electric energy consumption registered in Spain over almost 10 years. Experimental results confirm the validity of our proposal since it outperforms all other forecasting techniques to which it has been compared.

A Formal Verification Framework for Security Issues of Blockchain Smart Contracts

Blockchain technology has attracted more and more attention from academia and industry recently. Ethereum, which uses blockchain technology, is a distributed computing platform and operating system. Smart contracts are small programs deployed to the Ethereum blockchain for execution. Errors in smart contracts will lead to huge losses. Formal verification can provide a reliable guarantee for the security of blockchain smart contracts. In this paper, the formal method is applied to inspect the security issues of smart contracts. We summarize five kinds of security issues in smart contracts and present formal verification methods for these issues, thus establishing a formal verification framework that can effectively verify the security vulnerabilities of smart contracts. Furthermore, we present a complete formal verification of the Binance Coin (BNB) contract. It shows how to formally verify the above security issues based on the formal verification framework in a specific smart contract. All the proofs are checked formally using the Coq proof assistant in which contract model and specification are formalized. The formal work of this paper has a variety of essential applications, such as the verification of blockchain smart contracts, program verification, and the formal establishment of mathematical and computer theoretical foundations.