Recent News & Awards
• Dec 2014: Awarded a DARPA grant to study complexity analysis NEW
• Oct 2014: Giving a talk at IBM PL Day
• Aug 2014: Conference Chair of LICS
2016, to be held in New York!
• July 2014: Talk
at CSL/LICS 2014
• June 2014: Awarded a grant
to work on concurrent languages and verification
• June 2014: Visiting Microsoft Research, visiting University College London, and attending PLDI
• May 2014: Awarded a grant (URCF) from the NYU Office of the Provost NEW
• Mar 2014: Our paper
was accepted to CSL/LICS 2014
• Mar 2014: Visiting Yale University
• Mar 2014: ICALP
2015 program committee NEW
• Mar 2014: Visiting Rice University
• Feb 2014: Talk at Cornell Systems Lunch
• Feb 2014: Our paper was accepted to PLDI'14
• May 2013: Our paper
accepted to OOPSLA'13
• Feb 2013: Our paper
accepted to PLDI'13
• Feb 2013: Seminar
at Queen Mary
• Jan 2013: Analysis&Logics chair at POPL
• Dec 2012: Our paper
accepted to TACAS'13
• Sep 2012: PC meeting for POPL
My research is centered around devising mathematical techniques
that aid the development of safe concurrent software, and applying
those techniques to realistic computer systems. I investigate how to
improve the way programmers create efficient software and ensure that
these programs behave correctly. To this end, I have made advances
along a spectrum of fields, ranging from systems/concurrency, to
foundational results in formal methods.
Selected Research Topics:
- Multicore Software Development -- I am concerned with
exploring advances in languages and language analysis that enable
engineers to safely produce software which consists of parallel
computation. My work includes
commutativity race detection (PLDI'14),
exploiting nondeterminism for parallelism (OOPSLA'13),
(ESOP'14, POPL'10, PODC'09, PPoPP'08, SPAA'08a),
and semantics of transactional memory
- Automatic Software Verification --
I have developed static and dynamic program analysis techniques in
order to better understand the performance, understand the behavior, discover bugs and
formally prove correctness of programs. My work includes
temporal logic verification of C/C++ programs
(PLDI'13, POPL'11, CAV'11, FMSD'12),
temporal verification of higher-order programs (LICS'14),
and symbolic complexity bound analysis (PLDI'09).
- Dynamic analysis of systems, including
tracing distributed systems (EuroSys'08), and
deadlock detection (SPAA'08b).
- Abhinav Tamaskar (PhD student at NYU), spring 2015
- Mario Alvarez (PhD student at UCSD), summer 2014
- Ruben Zaccaroni (undergraduate at NYU), fall 2014
- Patrick Yuen (undergraduate at NYU), fall 2014
- PhD, Computer Science, University of Cambridge, 2012. Gates Scholarship.
- Sc.M, Computer Science, Brown University, 2008.
- B.S., Highest Honors, Computer Science and Physics, College of William & Mary, 2001.
- Visiting Assistant Professor, New York University
- Visiting Professor, Nagoya University, Japan
- Research Scientist & Principal Investigator, New York University
- Research Intern, Microsoft Research Cambridge
- Research Intern, Microsoft Research Redmond
- Adjunct Faculty, Newbury College
- Software Engineer at Amazon.com/ IMDb
- DARPA award to study complexity analysis NEW
- NSF Award to work on concurrent languages and verification
- Office of the Provost, New York University. $ 17,000. June 2014.
- Japan Society for Promotion of Science (JSPS). 1,000,000 JPY. September
- Japan Advanced Institute of Science & Technology (JAIST),
- Tel-Aviv University, Israel, (exp.) 2015.
- Microsoft Research, Cambridge, UK, Local Temporal Reasoning, July 2014.
- University College, London, UK, Local Temporal Reasoning, July 2014.
- Yale University, Local Temporal Reasoning, Mar 2014.
- Rice University, Local Temporal Reasoning, Mar 2014.
- Cornell University, Local Temporal Reasoning, Feb 2014.
- IBM Research, New York, Local Temporal Reasoning, Feb 2014.
- NYU, New York, Local Temporal Reasoning, Jan 2014.
- Tokyo University, Japan, Temporal verification of programs, May 2013.
- Nagoya University, Japan, Temporal verification of programs, Apr 2013.
- ETH Zurich, Switzerland, Commutativity Race Detection, Feb 2013.
- Queen Mary University, London, Specialization for Synchronization, Feb 2013.
- NEC Research, Reasoning about Nondeterminism in Programs, Mar 2013.
- Microsoft Research, A Theory of Serializabile Transactions, Nov 2012.
- CMACS NSF PI Meeting, Reasoning about Nondeterminism in Programs, Oct 2012.
- IBM PL Day, Reasoning about Nondeterminism in Programs, Jun 2012.
- High Confidence Software and Systems, Reasoning about Nondeterminism in Programs, May 2012.
- Vienna Sci. Tech. Fund, Austria, Data-structure Commutativity for
Multicore Processing, Dec 2011.
- NJPLS, Reasoning about Nondeterminism in Programs, Oct 2011.
- IBM TJ Watson Research Lab, Systems Code Verification: A Moving Target, Apr 2011.
- RiSE Seminar, IST Austria, Systems Code Verification: A Moving Target, Apr 2011.
- Microsoft Research Cambridge, Systems Code Verification: A Moving Target, Mar 2011.
- Oxford University, Branching-time reasoning for general-purpose programs, May 2010.
- University of Maryland, Making prophecies with decision predicates, May 2010.
- IBM TJ Watson Research Lab, Making prophecies with decision predicates, Feb 2010.
- Sun Microsystems, Boston.
- The College of William & Mary, Symbolic
bound analysis, February 12, 2009.
- Queen Mary University of London, Symbolic bound analysis, Dec 2008.
- Microsoft Research, Symbolic bound analysis, September 2008.