Our research has been generously supported by the following sponsors:
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, our papers and presentations, or by hiring our former students,
please consider sponsoring our research lab.
Complete Publications List (DBLP, Scholar)
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
- André Nascimento, IST/UL.
- Diogo Venâncio, IST/UL.
- Henrique Preto, IST/UL.
- João Silveira, IST/UL.
- Lucian Popescu, Politehnica University of Bucharest.
- Manuel Brito, IST/UL.
- Susana Monteiro, IST/UL.
- National body representative (of Portugal) in the ISO/IEC JTC 1/SC 22 committee (programming languages), and in its WG21 (C++)
- Local 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'20, SAS'18, FMCAD'14, DAC'14, CAV'14, ESOP'11, PASTE'10
- External reviewer: ERC grants 2018
- 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