???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
Produções

Publicações

Artigo em conferência
  1. Lopes, Nuno P.; Lee, Juneyoung; Hur, Chung-Kil; Liu, Zhengyang; Regehr, John. "Alive2: bounded translation validation for LLVM". 2021.
    10.1145/3453483.3454030
  2. Bjørner, Nikolaj; Levatich, Maxwell; Lopes, Nuno P.; Rybalchenko, Andrey; Vuppalapati, Chandrasekar. "Supercharging Plant Configurations Using Z3". 2021.
    10.1007/978-3-030-78230-6_1
  3. Lee, Juneyoung; Kim, Dongjoo; Hur, Chung-Kil; Lopes, Nuno P.. "An SMT Encoding of LLVM’s Memory Model for Bounded Translation Validation". 2021.
    10.1007/978-3-030-81688-9_35
  4. Lee, Juneyoung; Hur, Chung-Kil; Lopes, Nuno P.. "AliveInLean: A Verified LLVM Peephole Optimization Verifier". 2019.
    10.1007/978-3-030-25543-5_25
  5. Lopes, Nuno P.; Rybalchenko, Andrey. "Fast BGP Simulation of Large Datacenters". 2019.
    10.1007/978-3-030-11245-5_18
  6. Liu, Hongqiang Harry; Zhu, Yibo; Padhye, Jitu; Cao, Jiaxin; Tallapragada, Sri; Lopes, Nuno P.; Rybalchenko, Andrey; Lu, Guohan; Yuan, Lihua. "CrystalNet". 2017.
    10.1145/3132747.3132759
  7. Lee, Juneyoung; Kim, Yoonseung; Song, Youngju; Hur, Chung-Kil; Das, Sanjoy; Majnemer, David; Regehr, John; Lopes, Nuno P.. "Taming undefined behavior in LLVM". 2017.
    10.1145/3062341.3062343
  8. Sinha, Rohit; Costa, Manuel; Lal, Akash; Lopes, Nuno P.; Rajamani, Sriram; Seshia, Sanjit A.; Vaswani, Kapil. "A design and verification methodology for secure isolated regions". 2016.
    10.1145/2908080.2908113
  9. Plotkin, Gordon D.; Bjørner, Nikolaj; Lopes, Nuno P.; Rybalchenko, Andrey; Varghese, George. "Scaling network verification using symmetry and surgery". 2016.
    10.1145/2837614.2837657
  10. Lopes, Nuno P.; Monteiro, José. "Weakest Precondition Synthesis for Compiler Optimizations". 2014.
    10.1007/978-3-642-54013-4_12
  11. Lopes, Nuno P.; Monteiro, José. "Automatic Equivalence Checking of UF+IA Programs". 2013.
    10.1007/978-3-642-39176-7_18
  12. Grebenshchikov, Sergey; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey. "Synthesizing software verifiers from proof rules". 2012.
    10.1145/2254064.2254112
  13. Grebenshchikov, Sergey; Gupta, Ashutosh; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey. "HSF(C): A Software Verifier Based on Horn Clauses". 2012.
    10.1007/978-3-642-28756-5_46
  14. Lopes, Nuno P.; Rybalchenko, Andrey. "Distributed and Predictable Software Model Checking". 2011.
    10.1007/978-3-642-18275-4_24
Artigo em revista
  1. Lee, Juneyoung; Hur, Chung-Kil; Jung, Ralf; Liu, Zhengyang; Regehr, John; Lopes, Nuno P.. "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. Lopes, Nuno P.; Menendez, David; Nagarakatte, Santosh; Regehr, John. "Practical verification of peephole optimizations with Alive". Communications of the ACM 61 2 (2018): 84-91. http://dx.doi.org/10.1145/3166064.
    10.1145/3166064
  3. Lopes, Nuno P.; Monteiro, José. "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. 2022. "Systems and methods for error recovery". Estados Unidos.
    Concedida/Emitida
  2. 2021. "Communications network node". Estados Unidos.
  3. 2021. "Network verification systems and methods". Estados Unidos.
  4. 2021. "Partitioning for an execution pipeline". Estados Unidos.
    Pendente