Nuno Lopes

Contact E-mail: nuno.lopes@ist.utl.pt / nlopes@microsoft.com Mail: Microsoft Research 21 Station Road Cambridge CB1 2FB United Kingdom Microsoft Research Cambridge

Internships

MSR offers internships all year round. If you are interested in compilers and/or verification and would like to intern with us, please drop me an email.

Publications

Last 5:

• An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation (CAV'21)
• Alive2: Bounded Translation Validation for LLVM (PLDI'21)
• AliveInLean: A Verified LLVM Peephole Optimization Verifier (CAV'19)
• Fast BGP Simulation of Large Datacenters (VMCAI'19)
• Reconciling High-Level Optimizations and Low-Level Code in LLVM (OOPSLA'18)

Complete Publications List (DBLP, Scholar)

Projects

Alive & Alive2 (Dashboard of pending LLVM issues; Online Alive2): Automatic Verification of LLVM Optimizations

CORK: Compiler Optimization Correctness Checking

HSF: A Software Verifier based on Horn Clauses

PSyCO: Precondition Synthesis for Compiler Optimizations

Other Stuff

Slides