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 HASLab

2019

Limits in categories of Vietoris coalgebras

Authors
Hofmann, D; Neves, R; Nora, P;

Publication
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

Abstract
Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one - intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. When the functor is restricted to some of the categories induced by these conditions, the resulting categories of coalgebras are even complete. As a practical application, we use these developments in the specification and analysis of non-deterministic hybrid systems, in particular to obtain suitable notions of stability and behaviour.

2019

Concurrency Debugging with MaxSMT

Authors
Terra Neves, M; Machado, N; Lynce, I; Manquinho, V;

Publication
THIRTY-THIRD AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTY-FIRST INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / NINTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE

Abstract
Current Maximum Satisfiability (MaxSAT) algorithms based on successive calls to a powerful Satisfiability (SAT) solver are now able to solve real-world instances in many application domains. Moreover, replacing the SAT solver with a Satisfiability Modulo Theories (SMT) solver enables effective MaxSMT algorithms. However, MaxSMT has seldom been used in debugging multi-threaded software. Multi-threaded programs are usually non-deterministic due to the huge number of possible thread operation schedules, which makes them much harder to debug than sequential programs. A recent approach to isolate the root cause of concurrency bugs in multi-threaded software is to produce a report that shows the differences between a failing and a non-failing execution. However, since they rely solely on heuristics, these reports can be unnecessarily large. Hence, reports may contain operations that are not relevant to the bug's occurrence. This paper proposes the use of MaxSMT for the generation of minimal reports for multi-threaded software with concurrency bugs. The proposed techniques report situations that the existing techniques are not able to identify. Experimental results show that using MaxSMT can significantly improve the accuracy of the generated reports and, consequently, their usefulness in debugging the root cause of concurrency bugs.

2019

An Ontology-Based Recommendation System for Context-Aware Network Monitoring

Authors
Silva, RF; Carvalho, P; Lima, SR; Sabucedo, LA; Santos Gago, JM; Silva, JMC;

Publication
WorldCIST (2)

Abstract
Current network management systems urge for a context-aware perspective of the provided network services and the underlying infrastructure usage. This need results from the heterogeneity of services and technologies in place, and from the massive traffic volumes traversing today’s networks. To reduce complexity and improve interoperability, monitoring systems need to be flexible, context-aware, and able to self-configure measurement points (MPs) according to network monitoring tasks requirements. In addition, the use of sampling techniques in MPs to reduce the amount of traffic collected, analysed and stored has become mandatory and, currently, distinct sampling schemes are available for use in operational environments. In this context, the main objective of this paper is the ontological definition of measurement requirements and components in sampling-based monitoring environments, with the aim of supporting an expert recommendation system able to understand context and identify the appropriate configuration rules to apply to a selection of MPs. In this way, the ontology, defining management needs, network measurement topology and sampling techniques, is described and explored considering several network management activities. A use case focusing on traffic accounting as monitoring task is also provided, demonstrating the expressiveness of the ontology and the role of the recommendation system in assisting context-aware network monitoring based on traffic sampling.

2019

Privacy and Data Protection Concerns Regarding the Use of Blockchains in Smart Cities

Authors
Ramos, LFM; Silva, JMC;

Publication
PROCEEDINGS OF THE 12TH INTERNATIONAL CONFERENCE ON THEORY AND PRACTICE OF ELECTRONIC GOVERNANCE (ICEGOV2019)

Abstract
In this work we investigate which aspects of data protection regulation must be carefully observed when implementing Blockchain-based projects in smart cities. This technology provides interesting properties and allows governments to develop flexible and innovative data management systems. Nevertheless, realizing the benefits of using Blockchains requires understanding the government processes along with the legal framework and political setting imposed on government. Though it is a buzzword, Blockchain may not always be the best solution for data processing, and carrying out a Data Protection Impact Assessment could allow an analysis of the necessity and proportionality of the mechanism. Furthermore, principles relating to security of data remain applicable to Blockchains. We discuss points of interaction between Blockchain technology and the European Union data protection framework, and provide recommendations on how to better develop Blockchain-based projects in smart cities. The findings of the study should provide public sector actors with a guideline to assess the real necessity and better format of a Blockchain-based application.

2019

Heterogeneous Implementation of a Voronoi Cell-Based SVP Solver

Authors
Falcao, G; Cabeleira, F; Mariano, A; Santos, LP;

Publication
IEEE ACCESS

Abstract
This paper presents a new, heterogeneous CPU+GPU attacks against lattice-based (post-quantum) cryptosystems based on the Shortest Vector Problem (SVP), a central problem in lattice-based cryptanalysis. To the best of our knowledge, this is the first SVP-attack against lattice-based cryptosystems using CPUs and GPUs simultaneously. We show that Voronoi-cell based CPU+GPU attacks, algorithmically improved in previous work, are suitable for the proposed massively parallel platforms. Results show that 1) heterogeneous platforms are useful in this scenario, as they increment the overall memory available in the system (as GPU's memory can be used effectively), a typical bottleneck for Voronoi-cell algorithms, and we have also been able to increase the performance of the algorithm on such a platform, by successfully using the GPU as a co-processor, 2) this attack can be successfully accelerated using conventional GPUs and 3) we can take advantage of multiple GPUs to attack lattice-based cryptosystems. Experimental results show a speedup up to 7.6x for 2 GPUs hosted by an Intel Xeon E5-2695 v2 CPU (12 cores x2 sockets) using only 1 core and gains in the order of 20% for 2 GPUs hosted by the same machine using all 22 CPU threads (2 are reserved for orchestrating the GPUs), compared to single-CPU execution using the entire 24 threads available.

2019

A Quantum Algorithm for Ray Casting using an Orthographic Camera

Authors
Alves, C; Santos, LP; Bashford Rogers, T;

Publication
PROCEEDINGS OF THE 2019 INTERNATIONAL CONFERENCE ON GRAPHICS AND INTERACTION (ICGI 2019)

Abstract
Quantum computing has the potential to provide solutions to many problems which are challenging or out of reach of classical computers. There are several problems in rendering which are amenable to being solved in quantum computers, but these have yet to be demonstrated in practice. This work takes a first step in applying quantum computing to one of the most fundamental operations in rendering: ray casting. This technique computes visibility between two points in a 3D model of the world which is described by a collection of geometric primitives. The algorithm returns, for a given ray, which primitive it intersects closest to its origin. Without a spatial acceleration structure, the classical complexity for this operation is O(N). In this paper, we propose an implementation of Grover's Algorithm (a quantum search algorithm) for ray casting. This provides a quadratic speed up allowing for visibility evaluation for unstructured primitives in O(root N). However, due to technological limitations associated with current quantum computers, in this work the geometrical setup is limited to rectangles and parallel rays (orthographic projection).

  • 93
  • 260