Nuno Lopes

my photo

Contact

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

Microsoft Research Cambridge

Publications

Last 5:

An SMT Encoding of LLVM's Memory Model for Bounded Translation Validation (CAV'21)
Supercharging Plant Configurations Using Z3 (CPAIOR'21)
Alive2: Bounded Translation Validation for LLVM (PLDI'21, Distinguished Paper Award)
AliveInLean: A Verified LLVM Peephole Optimization Verifier (CAV'19)
Fast BGP Simulation of Large Datacenters (VMCAI'19)

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