About

I am a member of the InnerEye team at Microsoft Research Cambridge.

My interests are in the design and analysis of reliable intelligent systems, and I am currently working on precise and robust medical image analysis for cancer treatment.

In the past, together with wonderful colleagues, I have worked on exploring various synergies between programming languages and machine learning: a) ML4PL: the use of machine learning techniques in program verification, specification inference via Bayesian analysis, and b) PL4ML: probabilistic programming via program analysis, and productivity tools for machine learning tasks. I have also built a number of programmer productivity tools, and this includes the Yogi software model checker for device drivers.

Projects

R2: A Probabilistic Programming System

Established: July 16, 2013

What is R2? R2 is a probabilistic programming system that uses powerful techniques from program analysis and verification for efficient Markov Chain Monte Carlo (MCMC) inference. The language that is used to describe probabilistic models in R2 is based on…

Infer.NET Fun

Established: April 2, 2012

"I think it's extraordinarily important that we in computer science keep fun in computing." Alan J. Perlis - ACM Turing Award Winner 1966. Infer.NET Fun turns the simple succinct syntax of F# into an executable modeling language for Bayesian machine…

The Yogi Project

Established: August 1, 2007

Yogi is a research project within the Rigorous Software Engineering group at Microsoft Research India on software property checking. Our goal is to build a scalable software property checker by systematically combining static analysis with testing. We believe that this…

Publications

2015

2014

2013

2012

2011

2010

Proofs from Tests
Nels E. Beckman, Aditya Nori, Sriram Rajamani, Robert J. Simmons, Sai Deep Tetali, Aditya V. Thakur, in IEEE Transactions on Software Engineering (special issue on the ISSTA 2008 best papers), IEEE, March 1, 2010, View abstract, Download PDF

2009

2008

2007

2006

2005

2004

2003

2001

Other

Program committees

Invited talks

Interns/Students

2015

  • Siddharth Ancha (IIT Guwahati): Robust Neural Networks
  • Osbert Bastani (Stanford University): Robust Neural Networks
  • Leonidas Lampropoulos (UPenn): Robust Neural Networks
  • Kuldeep Singh Meel (Rice University): Robust MCMC sampling

2014

  • Aleksandar Chakarov (UC Boulder): Debugging machine learning tasks
  • Sulekha Kulkarni (Georgia Tech): Probabilistic programming
  • Shayak Sen (CMU): Debugging machine learning tasks
  • Vipul Venkataraman (IIT Bombay): Hamiltonian Monte Carlo sampling
  • Deepak Vijaykeerthy (IIT Madras): Debugging machine learning tasks

2013

  • Aparna Garimella (IIT Madras): Probabilistic programming
  • Sherjil Ozair (IIT Delhi): Synthesis of probabilistic programs
  • Selva Samuel (Anna University): Probabilistic programming with R2
  • Varun Tulsian (IISc Bangalore): Multiplexing program verifiers

2012

  • Arun Chaganty (Stanford University): Efficiently Sampling Probabilistic Programs via Program Analysis
  • Prasanth Chatarasi (IIT Hyderabad): Techniques for Combining Testing and Verification for Efficient Assertion Checking in Sequential Programs (Btech thesis)
  • Ravi Chirravuri (BITS Pilani): Scalability Heuristics for Program Verification (Btech thesis)
  • Guillaume Claret (ENS, Paris): Bayesian Inference for Probabilistic Programs via Symbolic Execution
  • Christian von Essen (Verimag, Grenoble): MCMC Sampling for Probabilistic Programs
  • Sivakanth Gopi (IIT Bombay): Compressed Sensing
  • Rahul Sharma (Stanford University): Program Termination via Machine Learning
  • Abhishek Udupa (UPenn): Distributed Software Model Checking

2011

  • Aws Albarghouthi (University of Toronto): Parallelizing Top-Down Interprocedual Analysis
  • Arun Chaganty (IIT Madras): Statistical Relational Learning
  • Vijay Victor D’Silva (Oxford University): Probabilistic Abstract Interpretation
  • Garvit Juniwal (IIT Bombay): Quantitative Label Inference
  • Robert J. Simmons (CMU): Sematics of Probabilistic Programs

2010

  • Nels E. Beckman (CMU): Specification inference for Plural
  • Abhishek Katyal (IIT Delhi): Automatic generation of environment models for software model checking
  • Matthias Heizmann (University of Frieburg): Verification of concurrent programs
  • Rahul Sharma (IIT Delhi): Relevance heuristics for software model checking (Btech thesis)
  • Rahul Srinivasan (IIT Bombay): Quantified Boolean Formulae solving
  • Zachery Tatlock (UCSD): Testing concurrent programs

2009

2008

2007

2006