openSDK: an open-source implementation of OPEN-R. - Nuno P. Lopes; Pedro U. Lima (AAMAS (3), 2008)

Optimizing Binary Code Produced by Valgrind (Project Report on Virtual Execution Environments Course - AVExe) - Filipe Cabecinhas; Nuno P. Lopes; Renato Crisostomo; Luís Veiga (CoRR, 2008)

Optimally Solving the MCM Problem Using Pseudo-Boolean Satisfiability - Nuno P. Lopes; Levent Aksoy; Vasco Manquinho; José Monteiro 001 (CoRR, 2010)

Applying Prolog to develop distributed systems. - Nuno P. Lopes; Juan Antonio Navarro Pérez; Andrey Rybalchenko; Atul Singh (Theory Pract. Log. Program., 2010)

Distributed and Predictable Software Model Checking. - Nuno P. Lopes; Andrey Rybalchenko (VMCAI, 2011)

Synthesizing software verifiers from proof rules. - Sergey Grebenshchikov; Nuno P. Lopes; Corneliu Popeea; Andrey Rybalchenko (PLDI, 2012)

HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). - Sergey Grebenshchikov; Ashutosh Gupta 001; Nuno P. Lopes; Corneliu Popeea; Andrey Rybalchenko (TACAS, 2012)

Automatic Equivalence Checking of UF+IA Programs. - Nuno P. Lopes; José Monteiro 001 (SPIN, 2013)

Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines. - Nuno Santos 001; Nuno P. Lopes (HotDep, 2014)

Weakest Precondition Synthesis for Compiler Optimizations. - Nuno P. Lopes; José Monteiro 001 (VMCAI, 2014)

Checking Beliefs in Dynamic Networks. - Nuno P. Lopes; Nikolaj S. Bjørner; Patrice Godefroid; Karthick Jayaraman; George Varghese (NSDI, 2015)

Provably correct peephole optimizations with alive. - Nuno P. Lopes; David Menendez; Santosh Nagarakatte; John Regehr (PLDI, 2015)

A design and verification methodology for secure isolated regions. - Rohit Sinha 001; Manuel Costa; Akash Lal; Nuno P. Lopes; Sriram K. Rajamani; Sanjit A. Seshia; Kapil Vaswani (PLDI, 2016)

Scaling network verification using symmetry and surgery. - Gordon D. Plotkin; Nikolaj S. Bjørner; Nuno P. Lopes; Andrey Rybalchenko; George Varghese (POPL, 2016)

Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. - Nuno P. Lopes; José Monteiro 001 (Int. J. Softw. Tools Technol. Transf., 2016)

Taming undefined behavior in LLVM. - Juneyoung Lee; Yoonseung Kim; Youngju Song; Chung-Kil Hur; Sanjoy Das; David Majnemer; John Regehr; Nuno P. Lopes (PLDI, 2017)

CrystalNet: Faithfully Emulating Large Production Networks. - Hongqiang Harry Liu; Yibo Zhu; Jitu Padhye; Jiaxin Cao; Sri Tallapragada; Nuno P. Lopes; Andrey Rybalchenko; Guohan Lu; Lihua Yuan (SOSP, 2017)

Practical verification of peephole optimizations with Alive. - Nuno P. Lopes; David Menendez; Santosh Nagarakatte; John Regehr (Commun. ACM, 2018)

Future Directions for Optimizing Compilers. - Nuno P. Lopes; John Regehr (CoRR, 2018)

Reconciling high-level optimizations and low-level code in LLVM. - Juneyoung Lee; Chung-Kil Hur; Ralf Jung 002; Zhengyang Liu 003; John Regehr; Nuno P. Lopes (Proc. ACM Program. Lang., 2018)

AliveInLean: A Verified LLVM Peephole Optimization Verifier. - Juneyoung Lee; Chung-Kil Hur; Nuno P. Lopes (CAV (2), 2019)

Fast BGP Simulation of Large Datacenters. - Nuno P. Lopes; Andrey Rybalchenko (VMCAI, 2019)

An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation. - Juneyoung Lee; Dongjoo Kim; Chung-Kil Hur; Nuno P. Lopes (CAV (2), 2021)

Supercharging Plant Configurations Using Z3. - Nikolaj S. Bjørner; Maxwell Levatich; Nuno P. Lopes; Andrey Rybalchenko; Chandrasekar Vuppalapati (CPAIOR, 2021)

Alive2: bounded translation validation for LLVM. - Nuno P. Lopes; Juneyoung Lee; Chung-Kil Hur; Zhengyang Liu 003; John Regehr (PLDI, 2021)

Torchy: A Tracing JIT Compiler for PyTorch. - Nuno P. Lopes (CC, 2023)

TCP: A Tensor Contraction Processor for AI Workloads Industrial Product. - Hanjoon Kim; Younggeun Choi; Junyoung Park; Byeongwook Bae; Hyunmin Jeong; Sang Min Lee 014; Jeseung Yeon; Minho Kim; Changjae Park; Boncheol Gu; Changman Lee; Jaeick Bae; et al. (ISCA, 2024)

Deferred Objects to Enhance Smart Contract Programming with Optimistic Parallel Execution. - George Mitenkov; Igor Kabiljo; Zekun Li 009; Alexander Spiegelman; Satyanarayana Vusirikala; Zhuolun Xiang; Aleksandar Zlateski; Nuno P. Lopes; Rati Gelashvili (CoRR, 2024)

FuriosaAI RNGD: A Tensor Contraction Processor for Sustainable AI Computing. - Younggeun Choi; Junyoung Park; Sang Min Lee 014; Jeseung Yeon; Minho Kim; Changjae Park; Byeongwook Bae; Hyunmin Jeong; Hanjoon Kim; June Paik; Nuno P. Lopes; Sungjoo Yoo (IEEE Micro, 2025)

Link-Time Optimization of Dynamic Casts in C++ Programs. - Xufan Lu; Nuno P. Lopes (Proc. ACM Program. Lang., 2025)

Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the Performance Impact. - Lucian Popescu; Nuno P. Lopes (Proc. ACM Program. Lang., 2025)