Hugo Pacheco

42 papers A* 3A 2B 5C 5Journal 18Unranked 8
YearRankTypeTitle / Venue / Authors
2025 A* conf
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
SP
José Bacelar Almeida, Gustavo Xavier Delerue Marinho Alves, Manuel Barbosa, Gilles Barthe, Luís Esquível, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub
2025 J jnl
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Gustavo Xavier Delerue Marinho Alves, Manuel Barbosa, Gilles Barthe, Luís Esquível, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub
2025 J jnl
Hyper model checking for high-level relational models.
CoRR
Nuno Macedo, Hugo Pacheco
2025 — conf
oCANada: A Generation-Based Fuzzer for ECUs over CAN.
VNC
Thales Santos, Patrick Grümer, Reza Parsamehr, Hugo Pacheco
2024 — conf
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.
CRYPTO (2)
José Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024 J jnl
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2023 J jnl
Formally verifying Kyber Episode IV: Implementation correctness.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
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
2023 J jnl
Formally verifying Kyber Part I: Implementation Correctness.
IACR Cryptol. ePrint Arch.
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
2023 A conf
General-Purpose Secure Conflict-free Replicated Data Types.
CSF
Bernardo Portela, Hugo Pacheco, Pedro Jorge, Rogério Pontes
2023 J jnl
General-Purpose Secure Conflict-free Replicated Data Types.
IACR Cryptol. ePrint Arch.
Bernardo Portela, Hugo Pacheco, Pedro Jorge, Rogério Pontes
2022 J jnl
A formal treatment of the role of verified compilers in secure computation.
J. Log. Algebraic Methods Program.
José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2021 A* conf
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
CCS
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2021 J jnl
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
CoRR
José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2021 J jnl
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2020 — conf
ROSY: An elegant language to teach the pure reactive nature of robot programming.
IRC
Hugo Pacheco, Nuno Macedo
2019 J jnl
ROSY: An elegant language to teach the pure reactive nature of robot programming.
CoRR
Hugo Pacheco, Nuno Macedo
2018 A conf
Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks.
CSF
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2018 J jnl
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2018 J jnl
Teaching how to program using automated assessment and functional glossy games (experience report).
Proc. ACM Program. Lang.
José Bacelar Almeida, Alcino Cunha, Nuno Macedo, Hugo Pacheco, José Proença
2017 J jnl
BiFluX: A Bidirectional Functional Update Language for XML.
Inf. Media Technol.
Tao Zan, Hugo Pacheco, Hsiang-Shang Ko, Zhenjiang Hu
2017 A* conf
Jasmin: High-Assurance and High-Speed Cryptography.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
2016 J jnl
A Tool-Chain for High-Assurance Cryptographic Software.
ERCIM News
José Bacelar Almeida, Manuel Barbosa, Hugo Pacheco, Vitor Pereira
2015 B conf
A Clear Picture of Lens Laws - Functional Pearl.
MPC
Sebastian Fischer, Zhenjiang Hu, Hugo Pacheco
2015 J jnl
The essence of bidirectional programming.
Sci. China Inf. Sci.
Sebastian Fischer, Zhenjiang Hu, Hugo Pacheco
2014 C conf
BiFluX: A Bidirectional Functional Update Language for XML.
PPDP
Hugo Pacheco, Tao Zan, Zhenjiang Hu
2014 B conf
Bidirectional spreadsheet formulas.
VL/HCC
Nuno Macedo, Hugo Pacheco, Nuno Rocha Sousa, Alcino Cunha
2014 C conf
Monadic combinators for "Putback" style bidirectional programming.
PEPM
Hugo Pacheco, Zhenjiang Hu, Sebastian Fischer
2014 — conf
Towards a Framework for Multidirectional Model Transformations.
EDBT/ICDT Workshops
Nuno Macedo, Alcino Cunha, Hugo Pacheco
2014 B conf
Validity Checking of Putback Transformations in Bidirectional Programming.
FM
Zhenjiang Hu, Hugo Pacheco, Sebastian Fischer
2014 — conf
Writing bidirectional model transformations as intentional updates.
ICSE Companion
Tao Zan, Hugo Pacheco, Zhenjiang Hu
2013 J jnl
A Generic Scheme and Properties of Bidirectional Transformations.
CoRR
Hugo Pacheco, Nuno Macedo, Alcino Cunha, Janis Voigtländer
2013 J jnl
Composing Least-change Lenses.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Nuno Macedo, Hugo Pacheco, Alcino Cunha, José Nuno Oliveira
2012 — conf
Bidirectional Transformation of Model-Driven Spreadsheets.
ICMT@TOOLS
Jácome Cunha, João Paulo Fernandes, Jorge Mendes, Hugo Pacheco, João Saraiva
2012 — —
Bidirectional data transformation by calculation
Hugo Pacheco
2012 J jnl
Delta Lenses over Inductive Types.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Hugo Pacheco, Alcino Cunha, Zhenjiang Hu
2012 — conf
Multifocal: A Strategic Bidirectional Transformation Language for XML Schemas.
ICMT@TOOLS
Hugo Pacheco, Alcino Cunha
2012 C conf
Relations as Executable Specifications: Taming Partiality and Non-determinism Using Invariants.
RAMiCS
Nuno Macedo, Hugo Pacheco, Alcino Cunha
2011 C conf
Calculating with lenses: optimising bidirectional transformations.
PEPM
Hugo Pacheco, Alcino Cunha
2010 B conf
Generic Point-free Lenses.
MPC
Hugo Pacheco, Alcino Cunha
2009 B conf
Mapping between Alloy Specifications and Database Implementations.
SEFM
Alcino Cunha, Hugo Pacheco
2008 — conf
Algebraic Specialization of Generic Functions for Recursive Types.
MSFP@ICALP
Alcino Cunha, Hugo Pacheco
2007 C conf
Coupled Schema Transformation and Data Conversion for XML and SQL.
PADL
Pablo Berdaguer, Alcino Cunha, Hugo Pacheco, Joost Visser