???global.info.a_carregar???
Identification

Personal identification

Full name
NUNO CLAUDINO PEREIRA LOPES

Citation names

  • Nuno P. Lopes

Author identifiers

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

Email addresses

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

Websites

Knowledge fields

  • Engineering and Technology - Electrotechnical Engineering, Electronics and Informatics
Education
Degree Classification
2014/07
Concluded
 Engenharia Informática e de Computadores (Doutoramento)
Major in Compiladores
Universidade de Lisboa Instituto Superior Técnico, Portugal
"Automatic Synthesis of Weakest Preconditions for Compiler Optimizations" (THESIS/DISSERTATION)
Affiliation

Science

Category
Host institution 		Employer
2014/09/01 - 2021/12/30 Principal Investigator (Research) Microsoft Research Ltd, United Kingdom
2013/03 - 2013/05 Research Trainee (Research) Microsoft Research, United States
2009/02 - 2009/07 Research Trainee (Research) Max-Planck-Institut für Softwaresysteme, Germany

Teaching in Higher Education

Category
Host institution 		Employer
2022/01/01 - Current Associate Professor (University Teacher) Universidade de Lisboa Instituto Superior Técnico, Portugal

Others

Category
Host institution 		Employer
2012/04 - 2012/07 Estágio Apple, Inc, United States
Projects

Contract

Designation Funders
2022/03/01 - 2023/12/01 Chameleon
0
Principal investigator
Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
 Google Inc
Concluded
2022/03/01 - 2023/03/01 Alive2
0
Principal investigator
Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal
 Woven Alpha
Concluded
Outputs

Publications

Conference paper
  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*". Paper presented in ISCA, 2024.
    10.1109/isca59077.2024.00069
  2. Nuno P. Lopes. Corresponding author: Nuno P. Lopes. "Torchy: A Tracing JIT Compiler for PyTorch". Paper presented in CC, 2023.
    10.1145/3578360.3580266
  3. Nuno P. Lopes; Lee, Juneyoung; Hur, Chung-Kil; Liu, Zhengyang; Regehr, John. Corresponding author: Nuno P. Lopes. "Alive2: bounded translation validation for LLVM". Paper presented in PLDI, 2021.
    10.1145/3453483.3454030
  4. Bjørner, Nikolaj; Levatich, Maxwell; Nuno P. Lopes; Rybalchenko, Andrey; Vuppalapati, Chandrasekar. "Supercharging Plant Configurations Using Z3". Paper presented in CPAIOR, 2021.
    10.1007/978-3-030-78230-6_1
  5. Lee, Juneyoung; Kim, Dongjoo; Hur, Chung-Kil; Nuno P. Lopes. Corresponding author: Nuno P. Lopes. "An SMT Encoding of LLVM’s Memory Model for Bounded Translation Validation". Paper presented in CAV, 2021.
    10.1007/978-3-030-81688-9_35
  6. Lee, Juneyoung; Hur, Chung-Kil; Nuno P. Lopes. Corresponding author: Nuno P. Lopes. "AliveInLean: A Verified LLVM Peephole Optimization Verifier". Paper presented in CAV, 2019.
    10.1007/978-3-030-25543-5_25
  7. Nuno P. Lopes; Rybalchenko, Andrey. Corresponding author: Nuno P. Lopes. "Fast BGP Simulation of Large Datacenters". Paper presented in 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". Paper presented in 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. Corresponding author: Nuno P. Lopes. "Taming undefined behavior in LLVM". Paper presented in 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". Paper presented in 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". Paper presented in POPL, 2016.
    10.1145/2837614.2837657
  12. Nuno P. Lopes; Monteiro, José. "Weakest Precondition Synthesis for Compiler Optimizations". Paper presented in VMCAI, 2014.
    10.1007/978-3-642-54013-4_12
  13. Lopes, Nuno P.; Monteiro, José. "Automatic Equivalence Checking of UF+IA Programs". Paper presented in 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". Paper presented in 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". Paper presented in TACAS, 2012.
    10.1007/978-3-642-28756-5_46
  16. Lopes, Nuno P.; Rybalchenko, Andrey. "Distributed and Predictable Software Model Checking". Paper presented in VMCAI, 2011.
    10.1007/978-3-642-18275-4_24
Journal article
  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. Corresponding author: 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é. Corresponding author: 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

Intellectual property

Patent
  1. Nuno P. Lopes. 2022. "Systems and methods for error recovery". United States.
    Granted/Issued
  2. Nuno P. Lopes; Rybalchenko, Andrey. 2021. "Communications network node". United States.
    Granted/Issued
  3. Nuno P. Lopes. 2021. "Network verification systems and methods". United States.
  4. Nuno P. Lopes. 2021. "Partitioning for an execution pipeline". United States.
    Granted/Issued
Activities

Supervision

Thesis Title
Role 		Degree Subject (Type)
Institution / Organization
2024/10 - Current Automatic Verification of Compiler Optimizations
Supervisor of Manuel Brito
Universidade de Lisboa Instituto Superior Técnico, Portugal
2023 - Current Link-time optimizations
Supervisor of Xufan Lu
Universidade de Lisboa Instituto Superior Técnico, Portugal
2016 - 2021 A validated semantics for LLVM IR
Co-supervisor of Juneyoung Lee
Seoul National University Department of Computer Science and Engineering, South Korea
Distinctions

Award

2024 Google Research Scholar Award
Google Inc, United States
2022 HiPEAC Tech Transfer Award
HiPEAC Network, Belgium

Other distinction

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