Abstract
The development of ETL systems has been the target of many research efforts to support its development and implementation. In the last few years, we presented a pattern-oriented approach to develop these systems. Basically, patterns are comprised by a set of abstract components that can be configured to enable its instantiation for specific scenarios. Even when using high-level components, the ETL systems are very specific processes that represent complex data requirements and transformation routines. Several operational requirements need to be configured and system correctness is hard to validate, which can result in several implementation problems. In this paper, a set of formal specifications in Alloy is presented to express the structural constraints and behaviour of a slowly changing dimension pattern. Then, specific physical models can be generated based on formal specifications and constraints defined in an Alloy model, helping to ensure the correctness of the configuration provided.

Abstract
This paper considers the single machine scheduling problem with weighted quadratic tardiness costs. Three metaheuristics are presented, namely iterated local search, variable greedy and steady-state genetic algorithm procedures. These address a gap in the existing literature, which includes branch-and-bound algorithms (which can provide optimal solutions for small problems only) and dispatching rules (which are efficient and capable of providing adequate solutions for even quite large instances). A simple local search procedure which incorporates problem specific information is also proposed. The computational results show that the proposed metaheuristics clearly outperform the best of the existing procedures. Also, they provide an optimal solution for all (or nearly all, in the case of the variable greedy heuristic) the smaller size problems. The metaheuristics are quite close in what regards solution quality. Nevertheless, the iterated local search method provides the best solution, though at the expense of additional computational time. The exact opposite is true for the variable greedy procedure, while the genetic algorithm is a good all-around performer.

Abstract
In this paper it is presented a music application for people with intellectual disabilities, called "Professor Piano". We created this application to be a solution for music education for this group of people. For that we present the development and implementation of the app. We choose the virtual piano and the mobile devices as the basis for our solution. It was conducted an assessment of the current status and features of mobile applications also using this paradigm, from which we concluded that, currently, there is not a virtual piano application oriented to people with intellectual disabilities so we design, develop and tested a new application, the "Professor Piano". To validate the "Professor Piano" application approach, we evaluated the application usage by a group of people with intellectual disabilities, without having too much user experience with mobile technologies, with the aim to measure the effectiveness, efficiency and satisfaction. We registered the following variables: success in a conclusion of a level (effectiveness); the percentage of correct notes played versus all notes of that level (efficiency); and the motivation at the end of the experience (satisfaction). The results obtained shows the interest and motivation of the users in playing with the application. In the four tests, three persons completed and wanted to continue the testing experience. This results also shows the importance of using an intuitive design and also of displaying the score at the end of each level, giving an extra boost to the user to replay or advance to the next level. © 2016 ACM.

Abstract
Cryptography is an inherently interdisciplinary area and the development of high-quality cryptographic software is a time-consuming task drawing on skills from mathematics, computer science and electrical engineering, only achievable by highly skilled programmers. The challenge is to map high-level cryptographic specifications phrased using mathematical abstractions into efficient implementations at the level of C or assembly that can be deployed on a target computational platform, whilst adhering to the specification both in terms of correctness and security. The High Assurance Software Laboratory at INESC-TEC maintains a domain-specific toolchain for the specification, implementation and verification of cryptographic software centred on CAO, a cryptography analyses and operations-aware language.

Abstract
Computer technologies are forever evolving and it is vital that computer science educators find new methods of teaching programming in order to maintain the rapid changes occurring in the field. One of the ways to increase student engagement and retention is by integrating games into the curriculum. Gamification-Based E-Learning Strategies for Computer Programming Education evaluates the different approaches and issues faced in integrating games into computer education settings. Featuring emergent trends on the application of gaming to pedagogical strategies and technological tactics, as well as new methodologies and approaches being utilized in computer programming courses, this book is an essential reference source for practitioners, researchers, computer science teachers, and students pursuing computer science.

Abstract
The recent advent of three-dimensional echocardiography has led to an increased interest from the scientific community in left ventricle segmentation frameworks for cardiac volume and function assessment. An automatic orientation of the segmented left ventricular mesh is an important step to obtain a point-To-point correspondence between the mesh and the cardiac anatomy. Furthermore, this would allow for an automatic division of the left ventricle into the standard 17 segments and, thus, fully automatic per-segment analysis, e.g. regional strain assessment. In this work, a method for fully automatic short axis orientation of the segmented left ventricle is presented. The proposed framework aims at detecting the inferior right ventricular insertion point. 211 three-dimensional echocardiographic images were used to validate this framework by comparison to manual annotation of the inferior right ventricular insertion point. A mean unsigned error of 8, 05° ± 18, 50° was found, whereas the mean signed error was 1, 09°. Large deviations between the manual and automatic annotations (> 30°) only occurred in 3, 79% of cases. The average computation time was 666ms in a non-optimized MATLAB environment, which potentiates real-Time application. In conclusion, a successful automatic real-Time method for orientation of the segmented left ventricle is proposed. © 2016 SPIE.