???global.info.a_carregar???
Identificação

Identificação pessoal

Nome completo
NUNO CLAUDINO PEREIRA LOPES

Nomes de citação

  • Nuno P. Lopes

Identificadores de autor

Ciência ID
131E-40D1-D00E
Google Scholar ID
DQnsjaoAAAAJ

Endereços de correio eletrónico

  • nuno.lopes@tecnico.ulisboa.pt (Profissional)

Websites

Domínios de atuação

  • Ciências da Engenharia e Tecnologias - Engenharia Eletrotécnica, Eletrónica e Informática
Formação
Grau Classificação
2014/07
Concluído
 Engenharia Informática e de Computadores (Doutoramento)
Especialização em Compiladores
Universidade de Lisboa Instituto Superior Técnico, Portugal
"Automatic Synthesis of Weakest Preconditions for Compiler Optimizations" (TESE/DISSERTAÇÃO)
Percurso profissional

Ciência

Categoria Profissional
Instituição de acolhimento 		Empregador
2014/09/01 - 2021/12/30 Investigador principal (carreira) (Investigação) Microsoft Research Ltd, Reino Unido
2013/03 - 2013/05 Estagiário de Investigação (Investigação) Microsoft Research, Estados Unidos
2009/02 - 2009/07 Estagiário de Investigação (Investigação) Max-Planck-Institut für Softwaresysteme, Alemanha

Docência no Ensino Superior

Categoria Profissional
Instituição de acolhimento 		Empregador
2022/01/01 - Atual Professor Associado (Docente Universitário) Universidade de Lisboa Instituto Superior Técnico, Portugal

Outros

Categoria Profissional
Instituição de acolhimento 		Empregador
2012/04 - 2012/07 Estágio Apple, Inc, Estados Unidos
Projetos

Projeto

Designação Financiadores
2022/03/01 - 2023/12/01 Chameleon
0
Investigador responsável
Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
 Google Inc
Concluído
2022/03/01 - 2023/03/01 Alive2
0
Investigador responsável
Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
 Woven Alpha
Concluído
Produções

Publicações

Artigo em conferência
  1. Kim, Hanjoon; Choi, Younggeun; Park, Junyoung; Bae, Byeongwook; Jeong, Hyunmin; Lee, Sang Min; Yeon, Jeseung; et al. "TCP: A Tensor Contraction Processor for AI Workloads Industrial Product*". Trabalho apresentado em ISCA, 2024.
    10.1109/isca59077.2024.00069
  2. Nuno P. Lopes. Autor correspondente: Nuno P. Lopes. "Torchy: A Tracing JIT Compiler for PyTorch". Trabalho apresentado em CC, 2023.
    10.1145/3578360.3580266
  3. Nuno P. Lopes; Lee, Juneyoung; Hur, Chung-Kil; Liu, Zhengyang; Regehr, John. Autor correspondente: Nuno P. Lopes. "Alive2: bounded translation validation for LLVM". Trabalho apresentado em PLDI, 2021.
    10.1145/3453483.3454030
  4. Bjørner, Nikolaj; Levatich, Maxwell; Nuno P. Lopes; Rybalchenko, Andrey; Vuppalapati, Chandrasekar. "Supercharging Plant Configurations Using Z3". Trabalho apresentado em CPAIOR, 2021.
    10.1007/978-3-030-78230-6_1
  5. Lee, Juneyoung; Kim, Dongjoo; Hur, Chung-Kil; Nuno P. Lopes. Autor correspondente: Nuno P. Lopes. "An SMT Encoding of LLVM’s Memory Model for Bounded Translation Validation". Trabalho apresentado em CAV, 2021.
    10.1007/978-3-030-81688-9_35
  6. Lee, Juneyoung; Hur, Chung-Kil; Nuno P. Lopes. Autor correspondente: Nuno P. Lopes. "AliveInLean: A Verified LLVM Peephole Optimization Verifier". Trabalho apresentado em CAV, 2019.
    10.1007/978-3-030-25543-5_25
  7. Nuno P. Lopes; Rybalchenko, Andrey. Autor correspondente: Nuno P. Lopes. "Fast BGP Simulation of Large Datacenters". Trabalho apresentado em VMCAI, 2019.
    10.1007/978-3-030-11245-5_18
  8. Liu, Hongqiang Harry; Zhu, Yibo; Padhye, Jitu; Cao, Jiaxin; Tallapragada, Sri; Nuno P. Lopes; Rybalchenko, Andrey; Lu, Guohan; Yuan, Lihua. "CrystalNet". Trabalho apresentado em SOSP, 2017.
    10.1145/3132747.3132759
  9. Lee, Juneyoung; Kim, Yoonseung; Song, Youngju; Hur, Chung-Kil; Das, Sanjoy; Majnemer, David; Regehr, John; Nuno P. Lopes. Autor correspondente: Nuno P. Lopes. "Taming undefined behavior in LLVM". Trabalho apresentado em PLDI, 2017.
    10.1145/3062341.3062343
  10. Sinha, Rohit; Costa, Manuel; Lal, Akash; Nuno P. Lopes; Rajamani, Sriram; Seshia, Sanjit A.; Vaswani, Kapil. "A design and verification methodology for secure isolated regions". Trabalho apresentado em PLDI, 2016.
    10.1145/2908080.2908113
  11. Plotkin, Gordon D.; Bjørner, Nikolaj; Nuno P. Lopes; Rybalchenko, Andrey; Varghese, George. "Scaling network verification using symmetry and surgery". Trabalho apresentado em POPL, 2016.
    10.1145/2837614.2837657
  12. Nuno P. Lopes; Monteiro, José. "Weakest Precondition Synthesis for Compiler Optimizations". Trabalho apresentado em VMCAI, 2014.
    10.1007/978-3-642-54013-4_12
  13. Lopes, Nuno P.; Monteiro, José. "Automatic Equivalence Checking of UF+IA Programs". Trabalho apresentado em SPIN, 2013.
    10.1007/978-3-642-39176-7_18
  14. Grebenshchikov, Sergey; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey. "Synthesizing software verifiers from proof rules". Trabalho apresentado em PLDI, 2012.
    10.1145/2254064.2254112
  15. Grebenshchikov, Sergey; Gupta, Ashutosh; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey. "HSF(C): A Software Verifier Based on Horn Clauses". Trabalho apresentado em TACAS, 2012.
    10.1007/978-3-642-28756-5_46
  16. Lopes, Nuno P.; Rybalchenko, Andrey. "Distributed and Predictable Software Model Checking". Trabalho apresentado em VMCAI, 2011.
    10.1007/978-3-642-18275-4_24
Artigo em revista
  1. Lee, Juneyoung; Hur, Chung-Kil; Jung, Ralf; Liu, Zhengyang; Regehr, John; Nuno P. Lopes. "Reconciling high-level optimizations and low-level code in LLVM". Proceedings of the ACM on Programming Languages 2 OOPSLA (2018): 1-28. http://dx.doi.org/10.1145/3276495.
    10.1145/3276495
  2. Nuno P. Lopes; Menendez, David; Nagarakatte, Santosh; Regehr, John. Autor correspondente: Nuno P. Lopes. "Practical verification of peephole optimizations with Alive". Communications of the ACM 61 2 (2018): 84-91.
    10.1145/3166064
  3. Nuno P. Lopes; Monteiro, José. Autor correspondente: Nuno P. Lopes. "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic". International Journal on Software Tools for Technology Transfer 18 4 (2015): 359-374. http://dx.doi.org/10.1007/s10009-015-0366-1.
    10.1007/s10009-015-0366-1

Propriedade Intelectual

Patente
  1. Nuno P. Lopes. 2024. "Compilation system and method". Estados Unidos.
    Concedida/Emitida
  2. Nuno P. Lopes. 2022. "Systems and methods for error recovery". Estados Unidos.
    Concedida/Emitida
  3. Nuno P. Lopes; Rybalchenko, Andrey. 2021. "Communications network node". Estados Unidos.
    Concedida/Emitida
  4. Nuno P. Lopes. 2021. "Network verification systems and methods". Estados Unidos.
    Concedida/Emitida
  5. Nuno P. Lopes. 2021. "Partitioning for an execution pipeline". Estados Unidos.
    Concedida/Emitida
Atividades

Orientação

Título / Tema
Papel desempenhado 		Curso (Tipo)
Instituição / Organização
2024/10 - Atual Automatic Verification of Compiler Optimizations
Orientador de Manuel Brito
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023 - Atual Link-time optimizations
Orientador de Xufan Lu
Universidade de Lisboa Instituto Superior Técnico, Portugal
2016 - 2021 A validated semantics for LLVM IR
Coorientador de Juneyoung Lee
Seoul National University Department of Computer Science and Engineering, Coreia do Sul
Distinções

Prémio

2024 Google Research Scholar Award
Google Inc, Estados Unidos
2022 HiPEAC Tech Transfer Award
HiPEAC Network, Bélgica

Outra distinção

2021 PLDI Distinguished Paper Award
Association for Computing Machinery, Estados Unidos
2015 PLDI Distinguished Paper Award
Association for Computing Machinery, Estados Unidos
2014 HVC Influential Work Award
Haifa Verification Conference, Israel