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 Alexandra Sofia Mendes

2009

Students' feedback on teaching mathematics through the calculational method

Authors
Ferreira, JF; Mendes, A;

Publication
Proceedings - Frontiers in Education Conference, FIE

Abstract
This paper describes a study conducted at the University of Nottingham, whose goal was to assess whether the students registered on the first-year module "Mathematics for Computer Scientists" appreciate the calculational method. The study consisted of two parts: "Proof Reading" and "Problem Solving". The goal of "Proof Reading" was to determine what the students think of calculational proofs, compared with more conventional ones, and which are easier to verify; we also assessed how their opinions changed during the term. The purpose of "Problem Solving" was to determine if the methods taught have influenced the students' problem-solving skills. Frequent criticisms of our approach are that we are too formal and that the emphasis on syntactic manipulation hinders students' understanding. Nevertheless, the results show that most students prefer or understand better the calculational proofs. On the other hand, regarding the problem-solving questions, we observed that, in general, the students maintained their original solutions. © 2009 Crown.

2009

Which Mathematics for the Information Society?

Authors
Ferreira, JF; Mendes, A; Backhouse, R; Barbosa, LS;

Publication
TEACHING FORMAL METHODS, PROCEEDINGS

Abstract
MathIS is a new project that aims to reinvigorate secondary-school mathematics by exploiting insights of the dynamics of algorithmic problem solving. This paper describes the main ideas that underpin the project. In summary, we propose a central role for formal logic, the development of a calculational style of reasoning, the emphasis on the algorithmic nature of mathematics, and the promotion of self-discovery by the students. These ideas are discussed and the case is made, through a number of examples that show the teaching style that we want to introduce, for their relevance in shaping mathematics training for the years to come. In our opinion, the education of software engineers that work effectively with formal methods and mathematical abstractions should start before university and would benefit from the ideas discussed here.

2011

Logic Training through Algorithmic Problem Solving

Authors
Ferreira, JF; Mendes, A; Cunha, A; Baquero, C; Silva, P; Barbosa, LS; Oliveira, JN;

Publication
TOOLS FOR TEACHING LOGIC

Abstract
Although much of mathematics is algorithmic in nature, the skills needed to formulate and solve algorithmic problems do not form an integral part of mathematics education. In particular, logic, which is central to algorithm development, is rarely taught explicitly at pre-university level, under the justification that it is implicit in mathematics and therefore does not need to be taught as an independent topic. This paper argues in the opposite direction, describing a one-week workshop done at the University of Minho, in Portugal, whose goal was to introduce to high-school students calculational principles and techniques of algorithmic problem solving supported by calculational logic. The workshop resorted to recreational problems to convey the principles and to software tools, the Alloy Analyzer and Netlogo, to animate models.

2014

Structure Editing of Handwritten Mathematics

Authors
Mendes, A; Backhouse, R; Ferreira, JF;

Publication
Proceedings of the Ninth ACM International Conference on Interactive Tabletops and Surfaces - ITS '14

Abstract

2017

Certified Password Quality

Authors
Ferreira, JF; Johnson, SA; Mendes, A; Brooke, PJ;

Publication
Lecture Notes in Computer Science - Integrated Formal Methods

Abstract

2017

Certified Password Quality - A Case Study Using Coq and Linux Pluggable Authentication Modules

Authors
Ferreira, JF; Johnson, SA; Mendes, A; Brooke, PJ;

Publication
Integrated Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings

Abstract
We propose the use of modern proof assistants to specify, implement, and verify password quality checkers. We use the proof assistant Coq, focusing on Linux PAM, a widely-used implementation of pluggable authentication modules for Linux. We show how password quality policies can be expressed in Coq and how to use Coq’s code extraction features to automatically encode these policies as PAM modules that can readily be used by any Linux system. We implemented the default password quality policy shared by two widely-used PAM modules: pam_cracklib and pam_pwquality. We then compared our implementation with the original modules by running them against a random sample of 100,000 leaked passwords obtained from a publicly available database. In doing this, we demonstrated a potentially serious bug in the original modules. The bug was reported to the maintainers of Linux PAM and is now fixed. © Springer International Publishing AG 2017.

  • 4
  • 6