Abstract
In a world where many human lives depend on the correct behavior of software systems, program verification assumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns. © 2018 IEEE.

Abstract
Demand response (DR) provides enormous opportunities to distribution system operators so as to conduct the power system in a sustainable manner. Due to the increasing penetration of electric vehicles (EV) in the power system, the necessity of enhancing flexibility has gained importance in the charging operation process. With the aid of the smart grid concept and DR programs, more flexible grid operations are provided. In this study, an optimal day-ahead EV charging strategy through electric vehicle parking lots (EVPL) aggregators is intended for the purpose of maximizing the load factor during daily operation. Furthermore, the behavioral uncertainty of EVs and peak load limitation based DR programs are also taken into account in the devised model. In order to reveal the effectiveness of the proposed EVPL aggregator energy management strategy, various case studies are performed, and credible results are reported.

Abstract
Understanding the role of the climate on the wine production is one of the major concerns of this sector since the environment usually determines the output of this industry. There are only a few previous studies that attempted to compile these environmental effects as an index, usually considering the temperature and the precipitation as their core variables. The present study suggests a new climate index which is based on descriptive statistics. Our index tries to mimic the target region characteristics and avoid the past studies premise of imposing previously conceived restrictions such as a fixed optimal climate. We then used yearly production and daily temperature data (1950-2016) from the Portuguese Minho wine region to test our proposed index and compare it with Ribéreau-Gayon and Peynaud (RGP, Ribéreau-Gayon et al., 2003) and Growing Degree-Days (GDD, Winkler et al., 1974) indexes. Our results showed that the newly proposed index may outperform the explanatory power of the other indexes and, in addition, may output interesting and unknown characteristics such as the different ideal temperatures regarding the studied region. © The Authors, published by EDP Sciences, 2018.

Abstract
The uncertainty and variability as a consequence of modern utilization of wind power in the electrical system besides unpredicted contingencies of the system components can impose crucial challenges on the Independent System Operator's (ISO) performance. In such a situation, increasing operational flexibility is the main way to cover wind power unpredictability and to enable secure operation of the power system. To this end, this paper proposes a flexible security-constrained program to schedule supply-side and demand-side via an optimal pricing and incentive scheme. The considered demand response (DR) programs include time of use (TOU), real-time pricing (RTP), critical peak pricing (CPP), as well as emergency demand response program (EDRP). The study aims to find the most effective DR scheme among a set of DR programs to improve the efficiency of electricity markets while guaranteeing the security and environmental restrictions through minimization of two objective functions, the ISO's operational cost and pollutant emissions from generation units.

Abstract

Abstract
The evolution of knowledge, where intellectual development and adaptive skills are required, has rendered the traditional rigid curricula and teaching methodologies outdated. Education and training must be acquired throughout life, hence the need to change the teaching-learning processes. The Bologna Process introduced new paradigms that resulted in curricula revisions, the reorganization of teaching-learning processes, the structuring of courses and curricular units. It shifted the teaching process to a new form that enhances and assesses the acquisition of learning skills based on the work performed by the students. It is student-centered teaching, where it is essential to define the intended levels of knowledge, how the students achieve them, and if they reach the necessary skills in each of those levels. Each student needs to be motivated to learn and to participate in the activities, which presupposes meaningful activities to arouse the interest in developing them. The purpose of this paper is to describe a design project, its implementation, orientation and effectiveness in problem-based learning (PBL). Another purpose is the establishment of a relationship between the Bologna process and the implicit implications in the structure of teaching and training in lighting projects. This paper presents a proposal of the use of Information and Communication Technologies (ICT) using DIALux evo software. It is part of the learning methodology, supported by computer simulation for lighting projects, in the Electrical Installation and Lighting Engineering Master's Degree in Service Engineering of Construction, 1st semester of the 1st year, in the Department of Electrical Engineering of the Institute of Engineering of Coimbra (ISEC). PBL combined with Flipped Classroom is used as a pedagogical strategy to enable higher education students to approach problems, in groups and with the supervision of a teacher, in order to acquire specialized knowledge. The implementation of the PBL method aimed at bringing education and learning closer to the professional reality of the future engineers. © 2018 IEEE.