???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

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
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. Nuno P. Lopes. Autor correspondente: Nuno P. Lopes. "Torchy: A Tracing JIT Compiler for PyTorch". Trabalho apresentado em CC, 2023.
    10.1145/3578360.3580266
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. Nuno P. Lopes; Monteiro, José. "Weakest Precondition Synthesis for Compiler Optimizations". Trabalho apresentado em VMCAI, 2014.
    10.1007/978-3-642-54013-4_12
  12. 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
  13. Grebenshchikov, Sergey; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey. "Synthesizing software verifiers from proof rules". Trabalho apresentado em PLDI, 2012.
    10.1145/2254064.2254112
  14. 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
  15. 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. 2022. "Systems and methods for error recovery". Estados Unidos.
    Concedida/Emitida
  2. Nuno P. Lopes; Rybalchenko, Andrey. 2021. "Communications network node". Estados Unidos.
    Concedida/Emitida
  3. Nuno P. Lopes. 2021. "Network verification systems and methods". Estados Unidos.
  4. Nuno P. Lopes. 2021. "Partitioning for an execution pipeline". Estados Unidos.
    Concedida/Emitida
Distinções

Prémio

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