Research

Pojects:

  • Currently working on optimizing the program synthesis tool Sketch.
  • QuaSy: Quantitative Synthesis tool for Control Systems.

Senior Undergraduate Thesis: Termination of Initialized Rational Linear Programs Rohit Singh, Supratik Chakraborty, IIT Bombay

Publications:

(Here’s my DBLP page.)

  1. Rohit Singh, Sumit Gulwani, Sriram Rajamani: Automatically Generating Algebra Problems. AAAI 2012 [PDF]
  2. Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, Rohit Singh: Quantitative Synthesis for Concurrent Programs. CAV 2011 [PDF]
  3. Krishnendu Chatterjee, Laurent Doyen, Rohit Singh: On Memoryless Quantitative Objectives. FCT 2011 [PDF]
  4. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh: QUASY: Quantitative Synthesis Tool. TACAS 2011: 267-271 [PDF]
  5. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann, Rohit Singh: Measuring and Synthesizing Systems in Probabilistic Environments. CAV 2010: 380-395 [PDF]

Past Research Experience:

  • Internship, Rigorous Software Engineering Group, Microsoft Research, Bangalore, India (June-July, 2011)
    Automatic problem and solution generation for Algebra problems
    Worked on designing a robust back-end for implementing a touch-based mobile application enabling high school students to manipulate trigonometric expressions and solve problems faster than the traditional pen and paper methods. We also devised a methodology to generate new problems similar to the given one with their solutions.
    With Sumit Gulwani, MSR Redmond and Sriram Rajamani, MSR Bangalore.

  • Internship, Institute of Science and Technology(IST), Austria (May-July, 2010)
    Quantitative Synthesis of Concurrent Data Structures
    We designed an algorithm for quantitative synthesis of synchronization constructs for concurrent data structure method sketches modeling them as solving games with imperfect information and implemented the algorithm for finding optimal concurrent list data structure lock-based synchronizations with respect to a weighted performance model.
    With Prof. Thomas Henzinger, Prof. Krishnendu Chatterjee, Pavol Cerny and Arjun Radhakrishnan

  • Internship, Ecole Polytechnique Federal de Lausanne(EPFL), Switzerland (May-July, 2009)
    Quantitative Synthesis of Reactive Systems
    Implemented the framework of quantitative synthesis of reactive systems using game-theoretic measures and extended the synthesis paradigm to incorporate probabilistic behavior of the environment. We also proposed a new polynomial time algorithm for solving parity mean payoff MDPs.
    With Prof. Thomas Henzinger and Barbara Jobstmann