Michael Carbin



I am an Assistant Professor of Electrical Engineering and Computer Science at MIT. I am interested in the semantics, design, and implementation of programming systems that operate in the presence of uncertainty: unreliable hardware, approximating compilers and runtimes, and nondeterministic/probabilistic environments.

From 2015-2018, I was a Researcher at Microsoft Research Redmond working on Large-Scale Deep Learning Systems, including both optimization and application.

News


  • Best Paper Award @ ICLR 2019
  • Ithemal accepted to ICML 2019
  • Google Faculty Award building on our work on Ithemal
  • Lottery Ticket Hypothesis accepted to ICLR 2019 with an Oral Presentation (24 of 500 accepted papers)
  • Leto accepted to OOPSLA 2018
  • Our work on computing with real numbers accepted to LICS 2018
  • 2018 NSF CAREER AWARD

Students


  • Current Graduate Students: Eric Atkinson, Jonathan Frankle, Alexander Renda, Benjamin Sherman, and Cambridge Yang
  • Current Undergraduate Students: Jesse Michel, Sahil Verma
  • Programming Systems Group Alumni: Brett Boston (MS, Aarno Labs)

Teaching


  • Dynamic Computer Language Engineering (6.S081), Spring 2019
  • Dynamic Computer Language Engineering (6.S081), Spring 2018
  • Computer Language Engineering (6.035), Fall 2017
  • (Dynamic) Computer Language Engineering (6.035), Spring 2017
  • Computer Systems Engineering (6.033), Spring 2016

Awards


  • Best Paper Award, ICLR 2019
  • Google Faculty Research Award, 2018
  • NSF CAREER Award, 2018
  • CACM Research Highlight, 2016
  • Best Paper Award, OOPSLA 2014
  • Best Paper Award, OOPSLA 2013
  • Best Talk Award, POPL Student Session 2013
  • Microsoft Research Graduate Fellowship, 2008
  • MIT Lemelson Presidential Fellowship, 2006
  • Stanford Wegbreit Best Computer Science Undergraduate Honors Thesis, 2006

Drafts


Stabilizing the Lottery Ticket Hypothesis
Jonathan Frankle, Gintare Karolina Dziugaite, Daniel M. Roy, and Michael Carbin (arXiv)

Verifying Handcoded Probabilistic Inference Procedures
Eric Atkinson, Cambridge Yang, and Michael Carbin (arXiv)

Publications


2019
Robust and sound solid modelling via arbitrary precision real arithmetic and continuity
Benjamin Sherman, Jesse Michel, and Michael Carbin
ICFP '19 (To Appear) — International Conference on Functional Programming

Ithemal: Accurate, Portable, and Fast Basic Block Throughput Estimation using Deep Neural Networks
Charith Mendis, Alex Renda, Saman Amarasinghe, and Michael Carbin
MLSys @ ISCA '19 (Best Paper) — Workshop on Machine Learning for Systems, co-located with ISCA
ICML '19 — International Conference on Machine Learning (arXiv)

Noise-Based Sensitivity Analysis of Programs
Jesse Michel, Sahil Verma, Benjamin Sherman, and Michael Carbin
WAX '19 — Workshop on Approximate Computing

Overparameterization: A Connection Between Software 1.0 and Software 2.0
Michael Carbin
SNAPL '19 — Summit on Advances in Programming Languages

The Lottery Ticket Hypothesis: Finding Small, Trainable Neural Networks
Jonathan Frankle and Michael Carbin
ICLR '19 (Best Paper) — International Conference on Learning Representations (arXiv)

2018
Leto: Verifying Application-Specific Fault Tolerance via First-Class Execution Models
Brett Boston, Zoe Gong, and Michael Carbin
OOPSLA '18 — Object-Oriented Programming, Systems, Languages, and Applications (draft)

Computable decision-making on the reals and other spaces via partiality and nondeterminism
Benjamin Sherman, Luke Sciarappa, Adam Chlipala, and Michael Carbin
LICS '18 — Logic in Computer Science

Constructive probabilistic semantics with non-spatial locales
Benjamin Sherman, Jared Tramontano, and Michael Carbin
PPS '18 — Probabilistic Program Semantics (paper)

2017
Optimizing Convolutional Neural Networks for Multicores for Scalability, Performance, and Goodput
Samyam Rajbhandari, Yuxiong He, Olatunji Ruwase, Michael Carbin, and Trishul Chilimbi
ASPLOS '17 — Architectural Support for Programming Languages and Operating Systems

2016
Towards Correct-by-Construction Probabilistic Inference
Eric Atkinson and Michael Carbin
NIPS MLS '16 — NIPS Workshop on Machine Learning Systems.

Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware
Michael Carbin, Sasa Misailovic, and Martin C. Rinard
CACM Research Highlight '16 — Communications of the ACM

2014
Chisel: Reliability- and Accuracy-Aware Optimization of Approximate Computational Kernels
Sasa Misailovic, Michael Carbin, Sara Achour, Zichao Qi, and Martin C. Rinard
OOPSLA '14 (Best Paper Award) — Object-Oriented Programming, Systems, Languages, and Applications.

2013
Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware
Michael Carbin, Sasa Misailovic, and Martin C. Rinard
OOPSLA '13 (Best Paper Award) — Object-Oriented Programming, Systems, Languages, and Applications.
Paper Slides
Press: Slashdot MITNews

Verified Integrity Properties for Safe Approximate Program Transformations
Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard
PEPM '13 — Partial Evaluation and Program Manipulation, co-located with POPL

2012
(Relative) Safety Properties for Relaxed Appproximate Programs
Michael Carbin and Martin C. Rinard
RACES '12 — Relaxing Synchronization for Multicore and Manycore Scalability,
co-located with OOPSLA

Cryptographic Path Hardening: Hiding Vulnerabilities in Software using Cryptography
Vijay Ganesh, Michael Carbin, and Martin C. Rinard
OBT '12 — Off the Beaten Track, co-located with POPL

Bolt: On-Demand Infinite Loop Escape in Unmodified Binaries
Michael Kling, Sasa Misailovic, Michael Carbin, and Martin C. Rinard
OOPSLA '12 — Object-Oriented Programming, Systems, Languages, and Applications
Paper Slides

Proving Acceptability Properties of Relaxed Nondeterministic Approximate Programs
Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard
PLDI '12 — Programming Language Design and Implementation
Paper Slides

Automatic Input Rectification
Fan Long, Vijay Ganesh, Michael Carbin, Stelios Sidirolgou, and Martin C. Rinard
ICSE '12 — International Conference on Software Engineering

2011
Detecting and Escaping Infinite Loops with Jolt
Michael Carbin, Sasa Misailovic, Michael Kling, and Martin C. Rinard
ECOOP '11 — European Conference on Object-Oriented Programming
Paper Appendix Slides
Press: Slashdot Ars Technica MIT News

Dynamic Knobs for Power-Aware Computing
Henry Hoffman, Stelios Sidiroglou, Michael Carbin, Sasa Misailovic,
Anant Agarwal, and Martin Rinard
ASPLOS '11 — Architectural Support for Programming Languages and Operating Systems
Paper

Automatically Identifying Critical Input Regions and Code Regions in Applications
Michael Carbin and Martin C. Rinard
ISSTA '10 — International Symposium of Software Testing And Analysis
Paper

Automatically Patching Errors in Deployed Software
Jeff H. Perkins, Sunghun Kim, Sam Larsen, Saman Amarasinghe, Jonathan Bachrach, Michael Carbin, Carlos Pacheco, Frank Sherwood, Stelios Sidiroglou, Greg Sullivan, Weng-Fai Wong, Yoav Zibin, Michael D. Ernst and Martin C. Rinard
SOSP '09 — Symposium on Operating Systems Principles
Press: Slashdot MIT News MIT Technology Review

Transactional Collection Classes
Brian D. Carlstrom, Austen McDonald, Michael Carbin, Christos Kozyrakis, and Kunle Olukotun
PPoPP '07 — Principles and Practice of Parallel Computing
Paper

Reflective Program Generation with Patterns
Manuel Fähndrich, Michael Carbin, James R. Larus
GPCE '06 — Generative Programming and Component Engineering
Paper

Using Datalog with Binary Decision Diagrams for Program Analysis
John Whaley, Dzintars Avots, Michael Carbin, Monica S. Lam
APLAS '05 — Asian Symposium Programming Languages and Systems 2005
Paper

Context-Sensitive Program Analysis as Database Queries
Monica S. Lam, John Whaley, V, Benjamin Livshits, Michael Martin, Dzintars Avots,
Michael Carbin, and Christopher Unkel
PODS '05 — Principles of Database Systems (Invited paper)
Paper

Theses and Technical Reports


Reasoning about Relaxed Programs
Michael Carbin, Deokwan Kim, Sasa Misailovic, Martin C. Rinard
Technical Report, MIT-CSAIL-TR-2011-050

Power-Aware Computing with Dynamic Knobs
Henry Hoffmann, Stelios Sidiroglou, Michael Carbin,
Sasa Misailovic, Anant Agarwal, and Martin Rinard
Tehcnical Report, MIT-CSAIL-TR-2010-027

Learning Effective BDD Variable Orders for BDD-Based Program Analysis
Michael Carbin
Stanford University Undergraduate Honors Thesis, May 2006
Paper

Patents


Configuration of Isolated Extensions and Device Drivers
Galen C. Hunt, James R. Larus, Manuel A. Fanndrich, Orion Hodson, David R. Tarditi, Michael Spear, Michael Carbin, Steven P. Levi, Bjarne Steensgaard
U.S. Patent Number 8,074,231. Filed: June 30, 2006. Issued: December 6, 2011

Bypass Virtualization
Thomas Joseph Purtell, Won Chun, Michael Carbin
U.S. Patent Number 8,065,687. Filed: Jan 7, 2008. Issued November 22, 2011

Contact


: mcarbin@csail.mit.edu
: Facebook
: LinkedIn
: Michael Carbin, MIT CSAIL, 77 Massachusetts Ave, 32-G782 Cambridge, MA 02139
: Office : (617) 253-5881