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.
Complete Publications List (DBLP, Scholar)
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