Publications of Nuno Lopes

  1. H. Kim, Y. Choi, J. Park, B. Bae, H. Jeong, S. M. Lee, J. Yeon, M. Kim, C. Park, B. Gu, C. Lee, J. Bae, S. Bae, Y. Cha, W. Choe, J. Choi, J. Ha, H. Han, N. Hwang, S. Hwang, K. Jang, H. Je, H. Jeon, J. Jeon, H. Jeong, Y. Jung, D. Kang, H. Kim, M. Kim, M. Kim, S. Kim, S. Kim, W. Kim, Y. Kim, Y. Kim, Y. Ku, J. K. Lee, J. Lee, K. Lee, S. Lee, M. Noh, H. Oh, G. Park, S. Park, J. Seo, J. Seong, J. Paik, N. P. Lopes, S. Yoo. TCP: A Tensor Contraction Processor for AI Workloads. In Proc. of the 51st International Symposium on Computer Architecture (ISCA), July 2024.
  2. N. P. Lopes. Torchy: A Tracing JIT Compiler for PyTorch. In Proc. of the ACM SIGPLAN 2023 International Conference on Compiler Construction (CC), Feb. 2023.
  3. J. Lee, D. Kim, C. Hur, N. P. Lopes. An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation. In Proc. of the 33rd International Conference on Computer-Aided Verification (CAV), July 2021.
  4. N. Bjørner, M. Levatich, N. P. Lopes, A. Rybalchenko, C. Vuppalapati. Supercharging Plant Configurations Using Z3. In Proc. of the 18th International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR), July 2021.
  5. N. P. Lopes, J. Lee, C. Hur, Z. Liu, J. Regehr. Alive2: Bounded Translation Validation for LLVM. In Proc. of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), June 2021 (Distinguished Paper Award).
  6. J. Lee, C. Hur, N. P. Lopes. AliveInLean: A Verified LLVM Peephole Optimization Verifier. In Proc. of the 31st International Conference on Computer-Aided Verification (CAV), July 2019.
  7. N. P. Lopes and A. Rybalchenko. Fast BGP Simulation of Large Datacenters. In Proc. of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan. 2019.
  8. J. Lee, C. Hur, R. Jung, Z. Liu, J. Regehr, N. P. Lopes. Reconciling High-Level Optimizations and Low-Level Code in LLVM. Proc. of the ACM on Programming Languages, Volume 2 Issue OOPSLA, Nov. 2018.
  9. N. P. Lopes, D. Menendez, S. Nagarakatte, J. Regehr. Practical Verification of Peephole Optimizations with Alive. Communications of the ACM, 61(2):84-91, Feb. 2018.
  10. H. H. Liu, Y. Zhu, J. Padhye, J. Cao, S. Tallapragada, N. P. Lopes, A. Rybalchenko, G. Lu, L. Yuan. CrystalNet: Faithfully Emulating Large Production Networks. In Proc. of the 26th Symposium on Operating Systems Principles (SOSP), Oct. 2017.
  11. J. Lee, Y. Kim, Y. Song, C. Hur, S. Das, D. Majnemer, J. Regehr, N. P. Lopes. Taming Undefined Behavior in LLVM. In Proc. of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2017.
  12. N. P. Lopes and J. Monteiro. Automatic Equivalence Checking of Programs with Uninterpreted Functions and Integer Arithmetic. International Journal on Software Tools for Technology Transfer, 18(4):359-374, Aug. 2016.
  13. R. Sinha, M. Costa, A. Lal, N. P. Lopes, S. Rajamani, S. A. Seshia, K. Vaswani. A Design and Verification Methodology for Secure Isolated Regions. In Proc. of the 37th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), June 2016.
  14. G. D. Plotkin, N. Bjørner, N. P. Lopes, A. Rybalchenko, G. Varghese. Scaling Network Verification using Symmetry and Surgery. In Proc. of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Jan. 2016.
  15. N. P. Lopes, D. Menendez, S. Nagarakatte, J. Regehr. Provably Correct Peephole Optimizations with Alive. In Proc. of the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), June 2015 (Distinguished Paper Award, SIGPLAN Research Highlight).
  16. N. P. Lopes, N. Bjørner, P. Godefroid, K. Jayaraman, G. Varghese. Checking Beliefs in Dynamic Networks. In Proc. of the 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI), May 2015.
  17. N. Santos and N. P. Lopes. Leveraging Trusted Computing and Model Checking to Build Dependable Virtual Machines. In Proc. of the 10th Workshop on Hot Topics in System Dependability (HotDep), Oct. 2014.
  18. N. P. Lopes. Automatic Synthesis of Weakest Preconditions for Compiler Optimizations. PhD thesis, Instituto Superior Técnico, July 2014.
  19. N. P. Lopes and J. Monteiro. Weakest Precondition Synthesis for Compiler Optimizations. In Proc. of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan. 2014.
  20. N. P. Lopes and J. Monteiro. Automatic Equivalence Checking of UF+IA Programs. In Proc. of the 20th International SPIN Symposium on Model Checking of Software, July 2013 (Best Paper Award).
  21. S. Grebenshchikov, N. P. Lopes, C. Popeea, A. Rybalchenko. Synthesizing Software Verifiers from Proof Rules. In Proc. of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2012 (HVC'14 Award).
  22. S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, A. Rybalchenko. HSF(C): A Software Verifier based on Horn Clauses (Competition Contribution). In Proc. of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Mar. 2012.
  23. N. P. Lopes and A. Rybalchenko. Distributed and Predictable Software Model Checking. In Proc. of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 340-355, Jan. 2011.
  24. N. P. Lopes, L. Aksoy, V. Manquinho, J. Monteiro. Optimally Solving the MCM Problem Using Pseudo-Boolean Satisfiability. Technical Report RT/43/2010, INESC-ID, Nov. 2010.
  25. N. P. Lopes, J. A. Navarro, A. Rybalchenko, A. Singh. Applying Prolog to Develop Distributed Systems. Theory and Practice of Logic Programming, 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue, 10(4-6):691-707, July 2010.
  26. N. P. Lopes. Practical Executable Specifications for Distributed Systems. Master thesis, Instituto Superior Técnico, Oct. 2009.
  27. F. Cabecinhas, N. P. Lopes, R. Crisóstomo, L. Veiga. Optimizing Binary Code Produced by Valgrind. Technical Report RT/46/2008, INESC-ID, Aug. 2008.
  28. N. P. Lopes and P. U. Lima. openSDK: an open-source implementation of OPEN-R. In Proc. of the 7th International Joint Conference on Autonomous Agents and MultiAgent Systems (AAMAS), pages 1207-1210, May 2008.
  29. L. Iocchi, L. Marchetti, R. Nardi, P. Lima, M. Barbosa, H. Pereira, N. P. Lopes. SPQR + ISocRob RoboCup 2007 Qualification Report. Technical Report, ISR Lisbon, 2007.
  30. P. Lima, M. Barbosa, J. Esteves, N. P. Lopes, V. d'Orey, H. Pereira. ISocRob-4LL 2006: Team Description Paper. Technical Report, ISR Lisbon, 2006.

 

<-- Go back home