Michael received his doctorate in Computer Science from UCLA in 2010 and joined Bell Labs in 2016, following a postdoc fellowship at the Paris 7 awarded by La Fondation Sciences Mathématiques de Paris (FSMP), and a faculty researcher position at the IMDEA Software Institute. Prior to all that, Michael completed his undergraduate studies at Binghamton University (SUNY). He has been a teaching assistant for undergraduate courses at UCLA and Paris 7, and has held internships at Microsoft Research, NASA Ames Research Center, and IBM.

Michael’s research enables the construction of reliable software by developing the foundations for effective programming abstractions and informative program analysis tools. Integrating technological trends with knowledge from several research communities spanning automata theory, programming languages, and distributed systems, his contributions include establishing the theoretical limits of program analysis, devising tractable approximations for intractable analysis problems, and building effective analysis tools.

Professional Activities

Program Committee TAPAS ’17
Program Committee CAV ’17
Program Committee FORTE ’17
Program Committee FoSSaCS ’17
Program Committee EC2 ’16
Program Committee FMCAD ’16
Program Committee NETYS ’16
External Review Committee POPL ’16
External Review Committee PPoPP ’16
Program Committee EC2 ’15
External Review Committee POPL ’15
Program Committee FM ’15
Program Chair EC2 ’14
External Review Committee PLDI ’14
External Review Committee POPL ’13
Program Committee VMCAI ’13
Program Committee Bytecode ’11


Verifying Constant-Time Implementations USENIX Security ’16
SMACK Software Verification Toolchain ICSE Companion ’16
Lock Allocation POPL ’07


SV-COMP ’15 award-winning bounded software verifier for C programs.
efficient symbolic reasoning algorithms for checking linearizability of concurrent data structures.
Boogie AST Manipulator which implements various code analyses and transformations for the Boogie intermediate verification language.
Minimizes input files via “delta debugging” by repeatedly “whittling” down features while maintaining validity.
save paper by printing every two pages of LNCS proceedings on a single page, without scaling.


Nokia Bell Labs
600 Mountain Ave., 2B-439
Murray Hill, NJ 07974
+1 (908) 743-4680