Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by CSE

2016

Exploring a Large News Collection Using Visualization Tools

Authors
Devezas, T; Devezas, JL; Nunes, S;

Publication
Proceedings of the First International Workshop on Recent Trends in News Information Retrieval co-located with 38th European Conference on Information Retrieval (ECIR 2016), Padua, Italy, March 20, 2016.

Abstract
The overwhelming amount of news content published online every day has made it increasingly difficult to perform macro-level analysis of the news landscape. Visual exploration tools harness both computing power and human perception to assist in making sense of large data collections. In this paper, we employed three visualization tools to explore a dataset comprising one million articles published by news organizations and blogs. The visual analysis of the dataset revealed that 1) news and blog sources evaluate very differently the importance of similar events, granting them distinct amounts of coverage, 2) there are both dissimilarities and overlaps in the publication patterns of the two source types, and 3) the content's direction and diversity behave differently over time. Copyright © 2016 for the individual papers by the paper's authors.

2016

Exploring educational immersive videogames: an empirical study with a 3D multimodal interaction prototype

Authors
Alves Fernandes, LMA; Matos, GC; Azevedo, D; Nunes, RR; Paredes, H; Morgado, L; Barbosa, LF; Martins, P; Fonseca, B; Cristovao, P; de Carvalho, F; Cardoso, B;

Publication
BEHAVIOUR & INFORMATION TECHNOLOGY

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.

2016

Verifying Constant-Time Implementations

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Emmi, M;

Publication
PROCEEDINGS OF THE 25TH USENIX SECURITY SYMPOSIUM

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.

2016

Enki: A Pedagogical Services Aggregator for Learning Programming Languages

Authors
Paiva, JC; Leal, JP; Peixoto Queirós, RA;

Publication
Proceedings of the 2016 ACM Conference on Innovation and Technology in Computer Science Education, ITiCSE 2016, Arequipa, Peru, July 9-13, 2016

Abstract
This paper presents Enki, a web-based IDE that integrates several pedagogical tools designed to engage students in learning programming languages. Enki achieves this goal (1) by sequencing educational resources, either expository or evaluative, (2) by using gamification services to entice students to solve activities, (3) by promoting social interaction and (4) by helping students with activities, providing feedback on submitted solutions. The paper describes Enki, its concept and architecture, details its design and implementation, and covers also its validation.

2016

A calculational approach to path-based properties of the Eisenstein-Stern and Stern-Brocot trees via matrix algebra

Authors
Ferreira, JF; Mendes, A;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
This paper proposes a calculational approach to prove properties of two well-known binary trees used to enumerate the rational numbers: the Stern-Brocot tree and the Eisenstein-Stern tree (also known as Calkin-Wilf tree). The calculational style of reasoning is enabled by a matrix formulation that is well-suited to naturally formulate path-based properties, since it provides a natural way to refer to paths in the trees. Three new properties are presented. First, we show that nodes with palindromic paths contain the same rational in both the Stern-Brocot and Eisenstein-Stern trees. Second, we show how certain numerators and denominators in these trees can be written as the sum of two squares x(2) and y(2), with the rational x/y appearing in specific paths. Finally, we show how we can construct Sierpifiski's triangle from these trees of rationals. (C) 2015 Published by Elsevier Inc.

2016

HDR video on mobile devices Unlocker of new opportunities for digital business

Authors
Melo, M; Barbosa, L; Meira, C; Branco, F; Bessa, M;

Publication
2016 11TH IBERIAN CONFERENCE ON INFORMATION SYSTEMS AND TECHNOLOGIES (CISTI)

Abstract
Prior to having available the High Dynamic Range (HDR) techniques, certain levels of luminance could only by captured by the human eye. Currently, HDR technology overcomes the limitations of conventional imaging technology (also referred as Low Dynamic Range or LDR) and allows the capture and delivery of contents that can match the dynamic range of the real world. However, the state of the art of HDR video focus mainly on conventional sized displays typical of TVs or PCs. As the usage of mobile devices for multimedia consumption is increasing considerably, there is a need for studying the impact of the viewing of HDR video on such devices. This will allow to take full advantage of HDR technology, creating a set of opportunities for the digital business as it allows, among others, the presentation of products in a much more efficient and captivating way. On this paper it is presented a study that evaluates the impact of the HDR video delivery on mobile devices and compares it with the impact of Low Dynamic Range (LDR) content. Results show that the delivery of HDR video on mobiles is possible without requiring much more resources when comparing the delivery of LDR video.

  • 174
  • 220