3 citations · 5 across the 3 of their papers we have counts for
6 papers
Towards Formal Verification of Password Generation Algorithms used in Password Managers
Miguel Grilo, João F. Ferreira, José Bacelar Almeida
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 w…
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head
José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy +3
MPC-in-the-Head (MitH) is a general framework that allows constructing efficient Zero Knowledge protocols for general NP-relations from secure multiparty computation (MPC) protocol…
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe +5
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected ag…
Formalization of context-free language theory
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira +1
Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, u…
Formalization of the pumping lemma for context-free languages
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira +1
Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid fo…
Deriving Sorting Algorithms
José Bacelar Almeida, Jorge Sousa Pinto
This paper proposes new derivations of three well-known sorting algorithms, in their functional formulation. The approach we use is based on three main ingredients: first, the algo…