Nuno Lopes

Contact E-mail: nuno.lopes@tecnico.ulisboa.pt Mail: INESC-ID, Office 134 Rua Alves Redol, 9 1000-029 Lisbon, Portugal Associate Professor @ Instituto Superior Técnico (Universidade de Lisboa) / INESC-ID Director @ FuriosaAI Portugal GitHub / Linkedin

Funding

Our research has been generously supported by the following sponsors:

• Google (€134k)
• Matter Labs ($10k)
• NLnet Foundation (€50k)
• Oracle (€44k in cloud credits)
• PRACE (800 GPU compute hours)
• RNCA (700 GPU compute hours)
• Woven by Toyota ($30k)

I thank the continuous support of all of our sponsors. Our work wouldn't be possible without their support.
If you and/or company have benefitted from our work, for example, by using our free tools, papers or presentations, or by hiring our former students, please consider sponsoring our research lab.

Publications

Last 5:

• Towards Removing Undef Values from LLVM IR (PLDI'26)
• Cpp2Rust: Automatic Translation of C++ to Safe Rust (PLDI'26)
• Translation Validation for LLVM's AArch64 Backend (OOPSLA'25)
• Pfeife: Automatic Pipeline Parallelism for PyTorch (ICML'25)
• Link-Time Optimization of Dynamic Casts in C++ Programs (PLDI'25)

Complete Publications List (DBLP, Scholar)

Slides

Current Projects

• Cpp2Rust: Automatic Translation of C++ to Safe Rust
• Alive2 (Dashboard of pending LLVM issues; Online Alive2): Automatic verification of LLVM optimizations

Prospective Students

I'm looking for great students that want to do Masters or PhD with me. Please get in touch if you are interested. Note that for Masters you must be enrolled with IST before contacting me.
Possible topics (non-exhaustive list):

• Compilers: IR design, scalable link-time optimizations, PGO, UB-aware optimizations
• Automatic software verification, namely of compilers (LLVM, MLIR, V8)
• Compilers and runtimes for machine learning frameworks like PyTorch or TensorFlow
• Code gen of machine learning kernels for many-core chips
• Law and regulations: formal specifications, model checking, optimization
• Security: automatic exploit generation, miscompilation exploitation
• Physical security: probablistic model checking
• Application of the Chinese Remainder theorem to SMT solving
• Blockchain mining: market efficiency (CPU/RAM/storage/network)
• Blockchain security: exploiting AMMs, compilers
• Trading/MM: volatily, cross-asset hedging, online ads

Current Students

PhD

• Ho Young Jhoo, Seoul National University.
• Lucian Popescu, IST/UL. Awards: “la Caixa” Foundation Doctoral INPhINIT fellowship.
• Xufan Lu, IST/UL.

MSc

• Francisco Gouveia, IST/UL.
• João Gouveia, IST/UL.

Former Students

PhD

• Juneyoung Lee, Seoul National University, 2021. A validated semantics for LLVM IR. Awards: student research competition (SRC) award at EuroLLVM'19, best PhD thesis award from the college of engineering of SNU.

MSc

• Pedro Lobo, IST/UL, 2025. Supporting raw data copies in the LLVM intermediate representation.
• Diogo Venâncio, IST/UL, 2024. A study on non-linear functions for quantization of machine learning models.
• João Silveira, IST/UL, 2024. Source-to-source optimization of safe Rust programs translated from C++.
• Lucian Popescu, Politehnica University of Bucharest, 2024. Performance impact of undefined behavior optimizations in C/C++.
• Manuel Brito, IST/UL, 2024. Optimistic global value numbering for compilers with undefined behavior.
• André Nascimento, IST/UTL, 2024. Cairo smart contract verification.
• George Mitenkov, ETH Zurich, 2023. Metering the meter, or how to efficiently and deterministically charge the execution of smart contracts.
• Henrique Preto, IST/UL, 2023. Automatic translation of C++ to Rust.
• Susana Monteiro, IST/UL, 2023. Static analysis for C++ Rust-like lifetime annotations. Awards: IST's young female alumna award.
• Sofia Salgueiro, IST/UL, 2021. Automatic synthesis of optimal datacenter networks.
• Kevin de Vos, IST/UL, 2020. Translation validation for the LLVM compiler.
• Filipe Azevedo, IST/UL, 2020. Evaluating value-wise poison values for the LLVM compiler.
• Janek van Oirschot, Eindhoven University of Technology, 2019. Extending tree pattern matching for application to peephole optimizations.

Academic Service

• National body representative (of Portugal) in the ISO/IEC JTC 1/SC 22 committee (programming languages), and in its WG21 (C++)
• Organization chair: FLoC'26
• Program committee: APLAS'23, PLDI'23, CGO'23, PLDI SRC'22, EuroLLVM'22, PLDI'21, VSTTE'20, VSTTE'19, PLDI'19, VSTTE'18, EuroLLVM'18, EuroLLVM'17, CGO'17, LLVM'15
• External review committee: POPL'17
• Reviewer: OOPSLA'25, PLDI'23, OOPSLA'20, SAS'18, FMCAD'14, DAC'14, CAV'14, ESOP'11, PASTE'10
• External reviewer: ERC grants 2018

Past Projects

• Alive: Automatic verification of LLVM peephole optimizations
• CORK: Compiler Optimization Correctness Checking
• HSF: An automatic software verifier based on Horn Clauses
• PSyCO: Precondition Synthesis for Compiler Optimizations
• Torchy: A tracing JIT compiler for PyTorch