Recent Publications

Pereira R, Carção T, Couto M, Cunha J, Fernandes JP, Saraiva J.  2017.  Helping Programmers Improve the Energy Efficiency of Source Code. Proceedings of the 39th International Conference on Software Engineering Companion. :238–240. Abstract
Pereira R.  2017.  Locating Energy Hotspots in Source Code. Proceedings of the 39th International Conference on Software Engineering Companion. :88–90. Abstract
Gonçalves R, Almeida PS, Moreno CB, Fonte V.  2017.  DottedDB: Anti-Entropy without Merkle Trees, Deletes without Tombstones. 36th IEEE International Symposium on Reliable Distributed Systems . Abstractdotteddb_srds.pdf

To achieve high availability in the face of network partitions, many distributed databases adopt eventual consistency, allow temporary conflicts due to concurrent writes, and use some form of per-key logical clock to detect and resolve such conflicts. Furthermore, nodes synchronize periodically to ensure replica convergence in a process called anti-entropy, normally using Merkle Trees. We present the design of DottedDB, a Dynamo-like key-value store, which uses a novel node-wide logical clock framework, overcoming three fundamental limitations of the state of the art: (1) minimize the metadata per key necessary to track causality, avoiding its growth even in the face of node churn; (2) correctly and durably delete keys, with no need for tombstones; (3) offer a lightweight anti-entropy mechanism to converge replicated data, avoiding the need for Merkle Trees. We evaluate DottedDB against MerkleDB, an otherwise identical database, but using per-key logical clocks and Merkle Trees for anti-entropy, to precisely measure the impact of the novel approach. Results show that: causality metadata per object always converges rapidly to only one id-counter pair; distributed deletes are correctly achieved without global coordination and with constant metadata; divergent nodes are synchronized faster, with less memory-footprint and with less communication overhead than using Merkle Trees.

Pontes R, Pinto M, Barbosa M, Vilaça R, Matos M, Oliveira R.  2017.  Performance trade-offs on a secure multi-party relational database. Proceedings of the Symposium on Applied Computing, {SAC} 2017, Marrakech, Morocco, April 3-7, 2017. :456–461. Abstract
Pontes R, Burihabwa D, Maia F, Paulo J, Schiavoni V, Felber P, Mercier H, Oliveira R.  2017.  SafeFS: a modular architecture for secure user-space file systems: one {FUSE} to rule them all. Proceedings of the 10th {ACM} International Systems and Storage Conference, {SYSTOR} 2017, Haifa, Israel, May 22-24, 2017. :9:1–9:12. Abstract
Nunes A, Couto R, Pacheco H, Bessa R, Gouveia C, Seca L, Moreira J, Nunes P, Matos P, Oliveira A.  2017.  Towards new data management platforms for a DSO as market enabler – UPGRID Portugal demo.
Proença J, Moreno CB.  2017.  Quality-Aware Reactive Programming for the Internet of Things. 7th IPM International Conference on Fundamentals of Software Engineering. quarp.pdf
He M, Vafeiadis V, Qin S, Ferreira JF.  2016.  Reasoning about Fences and Relaxed Atomics. Search Results 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing. Abstract2016-pdp-gpsfences.pdf

For efficiency reasons, weak (or relaxed) memory is now the norm on modern architectures. To cater for this trend, modern programming languages are adapting their memory models. The new C11 memory model allows several levels of memory weakening, including non-atomics, relaxed atomics, release-acquire atomics, and sequentially consistent atomics. Under such weak memory models, multithreaded programs exhibit more behaviours, some of which would have been inconsistent under the traditional strong (i.e. sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, recently developed by Turon et al., has made a step forward towards tackling this challenge. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release-acquire atomics. In this paper, we present a program logic, an enhancement of the GPS framework, that can support the verification of a bigger class of C11 programs, that is, programs with release-acquire atomics, relaxed atomics and release-acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of newly-designed verification rules.

Even C, Bosser A-G, Ferreira JF, Buche C, Stéphan F, Cavazza M, Lisetti C.  2016.  Supporting Social Skills Rehabilitation with Virtual Storytelling. 29th International FLAIRS Conference. Abstract12953-57659-1-pb.pdf

Social skills training (SST) has recently emerged as a typical application for emotional conversational agents (ECA). While a number of prototypes have targeted the general population, fewer have been used for psychiatric patients despite the widely recognised potential of ECAs technologies in the field of mental health. Social cognition impairment is however a widely shared symptom in psychiatric patients suffering from pathologies such as schizophrenia. Going further than SST, rehabilitation programmes involving role-play, but also problem solving have been successfully used by clinicians, drastically improving the quality of life of patients suffering from such disabilities. One of the challenges of these programmes is to ensure that the patients will be able to adapt their behaviour when the situation varies, rather than training them with the appropriate behaviour for a set of specific situations.
In this paper, we describe a novel approach for the development of a serious game supporting rehabilitation programmes for social skills, which will primarily target schizophrenia patients. We propose to use an ECA in combination with a narrative generation engine issued from interactive storytelling research to provide varied situations. This approach reflects the combination of both role-play and problem solving exercises on which remediation therapies rely, and has the potential to support patient's progress and motivation through the rehabilitation programme.

Couto R, Ribeiro AN, Campos JC.  2016.  Validating an approach to formalize use cases with ontologies. Proceedings of the 13th International Workshop on Formal Engineering Approaches to Software Components and Architectures. 205:1-15. Abstract1603.08632v1.pdf

Use case driven development methodologies put use cases at the center of the software development process. However, in order to support automated development and analysis, use cases need to be appropriately formalized. This will also help guarantee consistency between requirements specifications and the developed solutions. Formal methods tend to suffer from take up issues, as they are usually hard to accept by industry. In this context, it is relevant not only to produce languages and approaches to support formalization, but also to perform their validation. In previous works we have developed an approach to formalize use cases resorting to ontologies. In this paper we present the validation of one such approach. Through a three stage study, we evaluate the acceptance of the language and supporting tool. The first stage focusses on the acceptance of the process and language, the second on the support the tool provides to the process, and finally the third one on the tool's usability aspects. Results show test subjects found the approach feasible and useful and the tool easy to use.

Moreno CB, Almeida PS, Lerche C.  2016.  The problem with embedded CRDT counters and a solution. PaPoC '16 Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data. abstractcounterpapocfinal.pdf
Zawirski M, Moreno CB, Zawirski M, Preguiça N, Shapiro M.  2016.  Eventually Consistent Register Revisited. Proceeding PaPoC '16 Proceedings of the 2nd Workshop on the Principles and Practice of Consistency for Distributed Data. mvreg_papoc_camera.pdf