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

• https://web.ist.utl.pt/nuno.lopes/ (Scholar)

Knowledge fields

• Engineering and Technology - Electrotechnical Engineering, Electronics and Informatics

	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)

Science

	Category Host institution	Employer
2014/09/01 - 2021/12/30	Principal Investigator (Research)	Microsoft Research Ltd, United Kingdom

Teaching in Higher Education

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

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

Publications

Conference paper

Nuno P. Lopes. Corresponding author: Nuno P. Lopes. "Torchy: A Tracing JIT Compiler for PyTorch". Paper presented in CC, 2023. 10.1145/3578360.3580266 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 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 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 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 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 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 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 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 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 Nuno P. Lopes; Monteiro, José. "Weakest Precondition Synthesis for Compiler Optimizations". Paper presented in VMCAI, 2014. 10.1007/978-3-642-54013-4_12 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 Grebenshchikov, Sergey; Lopes, Nuno P.; Popeea, Corneliu; Rybalchenko, Andrey. "Synthesizing software verifiers from proof rules". Paper presented in PLDI, 2012. 10.1145/2254064.2254112 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 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

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

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

Award

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