O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Publicações

## Publicações por Alexandra Sofia Mendes

2016

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

Autores
Ferreira, JF; Mendes, A;

Publicação
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.

2014

### The magic of algorithm design and analysis: teaching algorithmic skills using magic card tricks

Autores
Ferreira, JF; Mendes, A;

Publicação
Innovation and Technology in Computer Science Education Conference 2014, ITiCSE '14, Uppsala, Sweden, June 23-25, 2014

Abstract
We describe our experience using magic card tricks to teach algorithmic skills to first-year Computer Science undergraduates. We illustrate our approach with a detailed discussion on a card trick that is typically presented as a test to the psychic abilities of an audience. We use the trick to discuss concepts like problem decomposition, pre- and post-conditions, and invariants. We discuss pedagogical issues and analyse feedback collected from students. The feedback has been very positive and encouraging. © 2014 ACM.

2018

### Towards Verified Handwritten Calculational Proofs

Autores
Mendes, A; Ferreira, JF;

Publicação
INTERACTIVE THEOREM PROVING, ITP 2018

Abstract
Despite great advances in computer-assisted proof systems, writing formal proofs using a traditional computer is still challenging due to mouse-and-keyboard interaction. This leads to scientists often resorting to pen and paper to write their proofs. However, when handwriting a proof, there is no formal guarantee that the proof is correct. In this paper we address this issue and present the initial steps towards a system that allows users to handwrite proofs using a pen-based device and that communicates with an external theorem prover to support the users throughout the proof writing process. We focus on calculational proofs, whereby a theorem is proved by a chain of formulae, each transformed in some way into the next. We present the implementation of a proof-of-concept prototype that can formally verify handwritten calculational proofs without the need to learn the specific syntax of theorem provers.

2019

### Lost in Disclosure: On the Inference of Password Composition Policies

Autores
Johnson, SA; Ferreira, J; Mendes, A; Cordry, J;

Publicação
IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops 2019, Berlin, Germany, October 27-30, 2019

Abstract
Large-scale password data breaches are becoming increasingly commonplace, which has enabled researchers to produce a substantial body of password security research utilising real-world password datasets, which often contain numbers of records in the tens or even hundreds of millions. While much study has been conducted on how password composition policies-sets of rules that a user must abide by when creating a password-influence the distribution of user-chosen passwords on a system, much less research has been done on inferring the password composition policy that a given set of user-chosen passwords was created under. In this paper, we state the problem with the naive approach to this challenge, and suggest a simple approach that produces more reliable results. We also present pol-infer, a tool that implements this approach, and demonstrates its use in inferring password composition policies. © 2019 IEEE.

2019

### Logic, Algebra, and Geometry at the Foundation of Computer Science

Autores
Hoare, T; Mendes, A; Ferreira, JF;

Publicação
Formal Methods Teaching - Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings

Abstract
This paper shows by examples how the Theory of Programming can be taught to first-year CS undergraduates. The only prerequisite is their High School acquaintance with algebra, geometry, and propositional calculus. The main purpose of teaching the subject is to support practical programming assignments and projects throughout the degree course. The aims would be to increase the student’s enjoyment of programming, reduce the workload, and increase the prospect of success. © 2019, Springer Nature Switzerland AG.

2020

### Skeptic: Automatic, Justified and Privacy-Preserving Password Composition Policy Selection

Autores
Johnson, SA; Ferreira, JF; Mendes, A; Cordry, J;

Publicação
ASIA CCS '20: The 15th ACM Asia Conference on Computer and Communications Security, Taipei, Taiwan, October 5-9, 2020

Abstract