Abstract

Abstract
Gestural interaction devices emerged and originated various studies on multimodal human-computer interaction to improve user experience (UX). However, there is a knowledge gap regarding the use of these devices to enhance learning. We present an exploratory study which analysed the UX with a multimodal immersive videogame prototype, based on a Portuguese historical/cultural episode. Evaluation tests took place in high school environments and public videogaming events. Two users would be present simultaneously in the same virtual reality (VR) environment: one as the helmsman aboard Vasco da Gama's fifteenth-century Portuguese ship and the other as the mythical Adamastor stone giant at the Cape of Good Hope. The helmsman player wore a VR headset to explore the environment, whereas the giant player used body motion to control the giant, and observed results on a screen, with no headset. This allowed a preliminary characterisation of UX, identifying challenges and potential use of these devices in multi-user virtual learning contexts. We also discuss the combined use of such devices, towards future development of similar systems, and its implications on learning improvement through multimodal human-computer interaction.

Abstract
The current Portuguese Tariff Code dates from December 2014 and requires that the Distribution Network Operators (DSO), submit to the Portuguese Energy Services Regulatory Agency, ERSE, a plan for a pilot experiment and a Cost Benefit Analysis (CBA) regarding the introduction of dynamic options in the Access Tariffs in Portugal. In view of this request, EDP Distribuicao, the main Portuguese DSO, established a contract with INESC TEC to conduct these studies and to prepare a report to submit to ERSE by June 2016. In this scope, this paper reports the results obtained so far namely regarding the CBA analysis. This analysis includes the identification of critical hours during which dynamic tariffs can be activated, the estimate of the impact of demand transfers to adjacent hours on the electricity market Social Welfare Function, on network losses, on the investment network avoided costs due to the possible deferral of reinforcements or expansions and on the costs of contracting reserves. These items were estimated along a period of 15 years and together with the estimate of the implementation costs of dynamic tariffs were used to conduct the mentioned CBA analysis.

Abstract
The constant-time programming discipline is an effective countermeasure against timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to constant-time programming is hard on its own, and extremely hard under additional efficiency and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software. We propose a novel approach for verifying constant-time security of real-world code. Our approach is able to validate implementations that locally and intentionally violate the constant-time policy, when such violations are benign and leak no more information than the public outputs of the computation. Such implementations, which are used in cryptographic libraries to obtain important speedups or to comply with legacy APIs, would be declared insecure by all prior solutions. We implement our approach in a publicly available, cross-platform, and fully automated prototype, ct-verif, that leverages the SMACK and Boogie tools and verifies optimized LLVM implementations. We present verification results obtained over a wide range of constant-time components from the NaCl, OpenSSL, FourQ and other off-the-shelf libraries. The diversity and scale of our examples, as well as the fact that we deal with top-level APIs rather than being limited to low-level leaf functions, distinguishes ct-verif from prior tools. Our approach is based on a simple reduction of constant-time security of a program P to safety of a product program Q that simulates two executions of P. We formalize and verify the reduction for a core high-level language using the Coq proof assistant.

Abstract

Abstract
Calendars are used daily by those who have an active social life, whether professional or personal. Although the calendar tends to have a personal connotation, there are many families who use it as the best way to manage their activities and organize family time, sharing by all the same calendar. Reconcile all events in one place shared without privacy commitment of each one, it becomes a difficult task. One option is to use a second calendar that puts the events that should not be shared within the family. However, this solution becomes slow for all events consultation. Thus, the proposed solution is the creation of a calendar, with three types of data display, to ensure that one can use it without compromising the privacy of each element. A web platform with a calendar and tasks to support these three types of exhibition was created and tested by families in their day to day over a period of time. The responses allowed to conclude that a calendar is a great memory aid as more than 80% use it to this end. The results obtained showed the needs that a user has when using a calendar as well as the willingness to use it in the family.