Conference Papers

Thread-aware logic programming for data-driven parallel programs

Cruz F., Rocha R., Goldstein S.C.

CEUR Workshop Proceedings

2015

Abstract:

Declarative programming in the style of functional and logic programming has been hailed as an alternative parallel programming style where computer programs are automatically parallelized without programmer control. Although this approach removes many pitfalls of explicit parallel programming, it hides important information about the underlying parallel architecture that could be used to improve the scalability and efficiency of programs. In this paper, we present a novel programming model that allows the programmer to reason about thread state in data-driven declarative programs. This abstraction has been implemented on top of Linear Meld, a linear logic programming language that is designed for writing graphbased programs. We present several programs that show the flavor of our new programming model, including graph algorithms and a machine learning algorithm. Our goal is to show that it is possible to take advantage of architectural details without losing the key advantages of logic programming.

Time and order estimation of paintings based on visual features and expert priors

Cabral R.S., Costeira J.P., De La Torre F., Bernardino A., Carneiro G.

Proceedings of SPIE - The International Society for Optical Engineering

2011

Abstract:

Time and order are considered crucial information in the art domain, and subject of many research efforts by historians. In this paper, we present a framework for estimating the ordering and date information of paintings and drawings. We formulate this problem as the embedding into a one dimension manifold, which aims to place paintings far or close to each other according to a measure of similarity. Our formulation can be seen as a manifold learning algorithm, albeit properly adapted to deal with existing questions in the art community. To solve this problem, we propose an approach based in Laplacian Eigenmaps and a convex optimization formulation. Both methods are able to incorporate art expertise as priors to the estimation, in the form of constraints. Types of information include exact or approximate dating and partial orderings. We explore the use of soft penalty terms to allow for constraint violation to account for the fact that prior knowledge may contain small errors. Our problem is tested within the scope of the PrintART project, which aims to assist art historians in tracing Portuguese Tile art “Azulejos” back to the engravings that inspired them. Furthermore, we describe other possible applications where time information (and hence, this method) could be of use in art history, fake detection or curatorial treatment.

TimeSHAP: Explaining Recurrent Models through Sequence Perturbations

Bento J., Saleiro P., Cruz A,, Figueiredo M., Bizarro P.

NeurIPS 2020

2020

Abstract:

Recurrent neural networks are a standard building block in numerous machine learning domains, from natural language processing to time-series classification. While their application has grown ubiquitous, understanding of their inner workings is still lacking. In practice, the complex decision-making in these models is seen as a black-box, creating a tension between accuracy and interpretability. Moreover, the ability to understand the reasoning process of a model is important in order to debug it and, even more so, to build trust in its decisions. Although considerable research effort has been guided towards explaining black-box models in recent years, recurrent models have received relatively little attention. Any method that aims to explain decisions from a sequence of instances should assess, not only feature importance, but also event importance, an ability that is missing from state-of-the-art explainers. In this work, we contribute to filling these gaps by presenting TimeSHAP, a model-agnostic recurrent explainer that leverages KernelSHAP’s sound theoretical footing and strong empirical results. As the input sequence may be arbitrarily long, we further propose a pruning method that is shown to dramatically improve its efficiency in practice.

Topology reconfiguration in Wi-Fi home networks

Nogueira J., Sargento S., Steenkiste P.

Proceedings of the 2013 IFIP/IEEE International Symposium on Integrated Network Management, IM 2013

2013

Abstract:

The use of Wi-Fi is booming in home networks and it is making it harder for the technology to cope with this exponential growth. The high-bandwidth requirement of streaming services, data backups and interactive cloud applications require solutions to improve the performance of the network while simultaneously simplifying its management. This paper unveils a new Wi-Fi management paradigm relying on dynamic network topology reconfiguration that adjusts the network topology to its traffic matrix, and mitigates the performance pitfalls inherent to Wi-Fi and its fixed topology. A linear programming formulation relying on cross-layer information is provided to assess the potential gains of such solution, and an evaluation is performed that explores the achievable performance and range extension gains. The simulation results show a significant increase in the wireless network capacity – up to two fold – as well as improvements in the network range.

Toward automatic classification of metadiscourse

Correia R., Mamede N., Baptista J., Eskenazi M.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

2014

Abstract:

This paper describes the supervised classification of four metadiscursive functions in English. Training data is collected using crowdsourcing to label a corpus of TED talks transcripts with occurrences of Introductions, Conclusions, Examples, and Emphasis. Using decision trees and lexical features, we report classification accuracy.

Towards a better understanding of distance-vector routing protocols with reset on failures

Quelhas T., Sobrinho J.L.

Proceedings of the 10th IASTED International Conference on Parallel and Distributed Computing and Networks, PDCN 2011

2011

Abstract:

We present a rigorous correctness proof, formalizable in temporal logic, for the distance vector with reset on failures protocol—an abstraction for a class of shortest-path routing protocols based on diffusing computations. This class includes the diffusing updates algorithm (DUAL), which is at the core of the Enhanced Interior Gateway Routing Protocol (EIGRP), widely used on the Internet. Our rigorous approach allows us to uncover counter-intuitive protocol behaviors which have not been reported previously. We also show that the protocol exhibits exponential message complexity under asynchronous operation, and discuss its applicability beyond shortest-path routing, in particular using the composite bandwidth-delay metric of EIGRP.

Towards Cloud Distributed Image Indexing by Sparse Hashing

Mourão A., Magalhães J.

Proceedings of the 2019 on International Conference on Multimedia Retrieval

2019

Abstract:

Distributing multimedia indexes to multiple nodes enables search over very large datasets (i.e., over one billion images and videos), but comes with a set of challenges: \textithow to distribute documents and queries effectively across nodes to support concurrent querying? andhow to deal with the increased potential for lack of response from nodes (e.g., node fail-stops or dropping of network packages)? An index where partitions are based on the distribution of feature vectors in the original space can improve redundancy and increase efficiency: nearest neighbors are only present on a small, set number of partitions, reducing the number of nodes to inspect for each query. This paper describes how sparse hashes can help find this balance and create better distribution policies for high-dimensional feature vectors. Inspired by existing literature on distributed text and media indexes, our proposal distributes and balances documents and queries to a subset of the nodes, according to their orthogonal similarities. We performed exhaustive benchmarks of our approach on a commercial cloud service. Experiments on a one billion vector dataset show that our approach has a low partitioning overhead (3 to 5 ms per query), achieves balanced document and query distribution (the variation in document and query distribution across nodes is smaller than 1% and 10%, respectively), handles concurrent queries effectively and degrades gracefully with node failures (less than 2% of precision loss per node down).

Towards concurrent type theory

Caires L., Pfenning F., Toninho B.

Conference Record of the Annual ACM Symposium on Principles of Programming Languages

2012

Abstract:

We review progress in a recent line of research that provides a concurrent computational interpretation of (intuitionistic) linear logic. Propositions are interpreted as session types, sequent proofs as processes in the pi-calculus, cut reductions as process reductions, and vice versa. The strong proof-theoretic foundation of this type system provides immediate opportunities for uniform generalization, specifically, to embed terms from a functional type theory. The resulting system satisfies the properties of type preservation, progress, and termination, as expected from a language derived via a Curry-Howard isomorphism. While very expressive, the language is strictly stratified so that dependent types for functional terms can be enforced during communication, but neither processes nor channels can appear in functional terms. We briefly speculate on how this limitation might be overcome to arrive at a fully dependent concurrent type theory.

Towards Formal Verification of Password Generation Algorithms used in Password Managers⋆

Grilo M., F. Ferreira J., Bacelar Almeida J.

arxiv

2021

Abstract:

Password managers are important tools that enable us to use stronger passwords, freeing us from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust password managers. In this paper, we focus on a feature that most password managers offer that might impact the user’s trust, which is the process of generating a random password. We survey which algorithms are most commonly used and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt as our framework to both specify the reference implementation and to prove its functional correctness and security.