Hugo José Pereira Pacheco


AuthID: R-001-JZH

Confirmed Publications: 36



1
TITLE: Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt
AUTHORS: Almeida, Jose Bacelar ; Alves, Gustavo Xavier Delerue Marinho; Barbosa, Manuel ; Barthe, Gilles; Esquivel, Luis; Hwang, Vincent; Oliveira, Tiago; Pacheco, Hugo ; Schwabe, Peter; Strub, Pierre Yves;
PUBLISHED: 2025, SOURCE: 2025 Symposium on Security and Privacy-SP in 2025 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, SP
INDEXED IN: Scopus WOS DBLP CrossRef
2
TITLE: Hyper model checking for high-level relational models
AUTHORS: Nuno Macedo; Hugo Pacheco ;
PUBLISHED: 2025, SOURCE: CoRR, VOLUME: abs/2512.12024
INDEXED IN: DBLP
IN MY: DBLP
3
TITLE: oCANada: A Generation-Based Fuzzer for ECUs over CAN
AUTHORS: Santos, Thales; Gruemer, Patrick; Parsamehr, Reza; Pacheco, Hugo ;
PUBLISHED: 2025, SOURCE: 16th Vehicular Networking Conference-VNC-Annual in 2025 IEEE VEHICULAR NETWORKING CONFERENCE, VNC
INDEXED IN: Scopus WOS DBLP
4
TITLE: Formally Verifying Kyber Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt
AUTHORS: Almeida, Jose Bacelar ; Olmos, Santiago Arranz; Barbosa, Manuel ; Barthe, Gilles; Dupressoir, Francois; Gregoire, Benjamin; Laporte, Vincent; Lechenet, Jean Christophe; Low, Cameron; Oliveira, Tiago; Pacheco, Hugo ; Quaresma, Miguel; Schwabe, Peter; Strub, Pierre Yves;
PUBLISHED: 2024, SOURCE: 44th Annual International Cryptology Conference on Advances in Cryptology (CRYPTO) in ADVANCES IN CRYPTOLOGY - CRYPTO 2024, PT II, VOLUME: 14921
INDEXED IN: Scopus WOS DBLP CrossRef: 12
5
TITLE: Formally verifying Kyber Episode IV: Implementation correctness. Episode IV: Implementation correctness
AUTHORS: José Bacelar Almeida ; Manuel Barbosa ; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean Christophe Léchenet; Tiago Oliveira; Hugo Pacheco ; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre Yves Strub;
PUBLISHED: 2023, SOURCE: IACR Trans. Cryptogr. Hardw. Embed. Syst., VOLUME: 2023, ISSUE: 3
INDEXED IN: Scopus DBLP CrossRef: 9
IN MY: ORCID
6
TITLE: General-Purpose Secure Conflict-free Replicated Data Types
AUTHORS: Portela, Bernardo ; Pacheco, Hugo ; Jorge, Pedro ; Pontes, Rogerio ;
PUBLISHED: 2023, SOURCE: IEEE 36th Computer Security Foundations Symposium (CSF) in 2023 IEEE 36TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM, CSF, VOLUME: 2023-July
INDEXED IN: Scopus WOS DBLP CrossRef: 2
IN MY: ORCID
7
TITLE: A formal treatment of the role of verified compilers in secure computation
AUTHORS: Bacelar Almeida, Jose Carlos ; Barbosa, Manuel ; Barthe, Gilles ; Pacheco, Hugo ; Pereira, Vitor; Portela, Bernardo ;
PUBLISHED: 2022, SOURCE: JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, VOLUME: 125
INDEXED IN: Scopus WOS DBLP CrossRef: 3
IN MY: ORCID
8
TITLE: Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head  Full Text
AUTHORS: José Carlos Bacelar Almeida ; Manuel Barbosa ; Karim Eldefrawy; Stéphane Graham Lengrand; Hugo Pacheco ; Vitor Pereira ;
PUBLISHED: 2021, SOURCE: ACM SIGSAC Conference on Computer and Communications Security (ACM CCS) in CCS '21: PROCEEDINGS OF THE 2021 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY
INDEXED IN: Scopus WOS DBLP CrossRef
9
TITLE: Rosy: An elegant language to teach the pure reactive nature of robot programming
AUTHORS: Hugo Pacheco ; Nuno Macedo ;
PUBLISHED: 2021, SOURCE: International Journal of Robotic Computing, VOLUME: 3, ISSUE: 1
INDEXED IN: CrossRef
10
TITLE: ROSY: An elegant language to teach the pure reactive nature of robot programming PDF
AUTHORS: Pacheco, H ; Macedo, N ;
PUBLISHED: 2020, SOURCE: 2020 FOURTH IEEE INTERNATIONAL CONFERENCE ON ROBOTIC COMPUTING (IRC 2020)
INDEXED IN: Scopus WOS DBLP arXiv CrossRef
Page 1 of 4. Total results: 36.

footer slogan

Useful Links

Get Help

© 2026 CRACS & Inesc TEC - All Rights Reserved Privacy Policy | Terms of Service