Abstract
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as handwritten assembly. We illustrate our approach using ChaCha20Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code. We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking. We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt.

Abstract
Data science has started to become one of the most important skills one can have in the modern world, due to data taking an increasingly meaningful role in our lives. The accessibility of data science is however limited, requiring complicated software or programming knowledge. Both can be challenging and hard to master, even for the simple tasks. With this in mind, we have approached this issue by providing a new data science platform, termed DS4All.Curation, that attempts to reduce the necessary knowledge to perform data science tasks, in particular for data cleaning and curation. By combining HCI concepts, this platform is: simple to use through direct manipulation and showing transformation previews; allows users to save time by eliminate repetitive tasks and automatically calculating many of the common analyses data scientists must perform; and suggests data transformations based on the contents of the data, allowing for a smarter environment. © 2020, Springer Nature Switzerland AG.

Abstract
In the era of industrial revolution 4.0, an automotive industry flourished in a way that was never before. As different features added in the driver assistance systems time-to-time, hence, nowadays the driving process is not so much tedious as it seems before. This ensures the operation of hassle-free driving, which leads towards autonomous vehicles. Overall, it opens up many opportunities for researchers and business communities, but at the same time, raises concerns and issues for discussion that need to be analyzed before put the final product (here, in the sense of fully automated vehicle) on the road. We conducted an online-survey (N = 3139) with participants from 146 nations was participated and assembled their valuable feedback on the automated driving and human presence in the autonomous vehicles considering all the levels of driving automation. This paper explores the results in terms of useful implications, which highlights and implied us to re-examine the present regulations and policies in automated driving and autonomous vehicles. © 2020, Springer Nature Switzerland AG.

Abstract

Abstract
The aim of the present study is to analyze brand resonance measures to assess reliability, dimensionality and validity using existing models of brand resonance. This study is based on a mixed approach of research methodology, using qualitative and quantitative methods. In the qualitative approach, we use expert interview and focus group discussion tools. In the quantitative approach, a corporate survey was conducted and 560 responses were collected through a structured questionnaire. The analysis is performed using statistical scaling tools such as Exploratory Factor Analysis (EFA) and Confirmatory Factor Analysis (CFA). This study initiated scale extraction and operationalization processes for 72 observed variables to measure nine latent variables and obtained 34 statistically extracted observed variables. The study provides a reliable and validated means to measure brand resonance constructs. The study develops a brand resonance scale, which can help brand managers to measure consumers' levels of brand resonance, in order to describe the strength of the bond of their consumer with their brand(s). This study develops empirically extracted measures of brand resonance, making it distinctive in the branding literature. The study also ensures all important aspects of measurement scale, such as validity and reliability.

Abstract
The appearance of the flexible behavior of end-users based on demand response programs makes the power distribution grids more active. Thus, electricity market participants in the bottom layer of the power system, wish to be involved in the decision-making process related to local energy management problems, increasing the efficiency of the energy trade in distribution networks. This paper proposes monopolistic and game-based approaches for the management of energy flexibility through end-users, aggregators, and the Distribution System Operator (DSO) which are defined as agents in the power distribution system. Besides, a 33-bus distribution network is considered to evaluate the performance of our proposed approaches for energy flexibility management model based on impact of flexibility behaviors of end-users and aggregators in the distribution network. According to the simulation results, it is concluded that although the monopolistic approach could be profitable for all agents in the distribution network, the game-based approach is not profitable for end-users.