Recent Publications

Oliveira JN, Macedo H.  2017.  The Data Cube As a Typed Linear Algebra Operator. Proc. of the 16th Int. Symposium on Database Programming Languages. :6:1–6:11. Abstract
n/a
Santos A, Cunha A, Macedo N, Arrais R, dos Santos FN.  2017.  Mining the Usage Patterns of ROS Primitives. Abstractros_patterns.pdf

The Robot Operating System (ROS) is nowadays one of the most popular frameworks for developing robotic
applications. To ensure the (much needed) dependability and safety of such applications we forecast an increasing demand for ROS-specific coding standards, static analyzers, and tools alike. Unfortunately, the development of such standards and tools can be hampered by ROS modularity and configurability, namely the substantial number of primitives (and respective variants) that must, in principle, be considered.
To quantify the severity of this problem, we have mined a large number of existing
ROS packages to understand how its primitives are used in practice, and to determine which combinations of primitives are most popular. This paper presents and discusses the results of this study, and hopefully provides some guidance for future standardization efforts and tool developers.
Cledou G, Proença J, Barbosa LS.  2017.  A Refinement Relation for Families of Timed Automata. XX Brazilian Symposium on Formal Methods. Abstractiftarefinement.pdf

Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typically parameterized by a set of features and a feature model that specifies the valid combinations of features. This paper explores how to safely replace such families of components with more refined ones. We propose a notion of refinement for Interface Featured Timed Automata (IFTA), a formalism to model families of timed automata with support for multi-action transitions. We separate the notion of IFTA refinement into behavioral and variability refinement, i.e., the refinement of the underlying timed automata and feature model. Furthermore, we define behavioral refinement for the semantic level, i.e., transition systems, as an alternating simulation between systems, and lift this definition to IFTA refinement. We illustrate this notion with examples throughout the text and show that refinement is a pre-order and compositional.
Shoker A.  2017.  Sustainable Blockchain through Proof of eXercise. The 16th IEEE International Symposium on Network Computing and Applications (NCA 2017). PoX
Kassam Z, Shoker A, Almeida PS, Moreno CB.  2017.  Aggregation Protocols in Light of Reliable Communication. The 16th IEEE International Symposium on Network Computing and Applications (NCA 2017). Aggregation Protocols in Light of Reliable Communication
Machado M, Couto R, Campos JC.  2017.  MODUS: model-based user interfaces prototyping. Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2017, Lisbon, Portugal, June 26-29, 2017. :111–116. Abstractmain.pdf

n/a
Carvalho M, Belo O, Macedo N.  2017.  Checking the Correctness of What-If Scenarios. 11th IFIP WG 8.9 Working Conference (CONFENIS 2017).
Silva JMC, Bispo KA, Carvalho P, Lima SR.  2017.  LiteSense: An adaptive sensing scheme for WSNs. 2017 IEEE Symposium on Computers and Communications (ISCC). :1209-1212. Abstract
n/a
Almeida JB, Barbosa M, Barthe G, Blot A, Grégoire B, Laporte V, Oliveira T, Pacheco H, Schmidt B, - P.  2017.  Jasmin: High-Assurance and High-Speed Cryptography. Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2017, Dallas, TX, USA, October 30 - November 03, 2017. :1807–1823. Abstract
n/a
Macedo R, Paulo J, Pontes R, Portela B, Oliveira T, Matos M, Oliveira R.  2017.  A Practical Framework for Privacy-Preserving NoSQL Databases. 36th {IEEE} Symposium on Reliable Distributed Systems, {SRDS} 2017, Hong Kong, Hong Kong, September 26-29, 2017. :11–20. Abstract
n/a
Couto R, Campos JC, Ribeiro AN.  2017.  Usability evaluation of the uCat tool. EPCGI. usability_ucat.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.