Programming Languages and Tools

Rigorous Software Engineering has evolved and changed its name! The new area is called : “Programming Languages and Tools (PLATO)”.

We work on tools, languages and methodologies to dramatically increase the productivity of software development. We are interested in both analysis tools for existing software, as well as in asking questions about how software of the future should be designed.

Current focus

Verification and Testing

We are working on static analysis and testing to find bugs in programs and also guarantee certain properties about programs: Yogi.

PASTA = Program Analysis + Statistical Analysis

We are working on a variety of techniques that combine information from programs together with a large amount of data about development process, as well data from users to help handle the information overload associated with large projects: DebugAdvisor, Holmes and Tark. We are also working on applications of Bayesian inference for specification inference, QBF solving and program synthesis: Merlin, other links coming soon.

Programming Models for Concurrency and Distribution

We are working on new techniques that help programmers write correct concurrent programs by construction, and better programming abstractions to deal with the realities of concurrency and distribution: WYPIWYG, Isolator, Guesstimate, Speculative Parallelism, Molecular Transactions.

RSE Tools Downloads

Guesstimate: Programming model for collaborative distributed systems
Holmes: Automated statistical debugging for .NET
Tark: Mining linear temporal rules

Past Projects

SLAM is a joint project with the SRR group at MSR. SLAM is the engine that drives Microsoft's Static Driver Verifier.
Preferential Path Profiling (PPP) is a joint project with the RAD group at MSR. PPP is a novel scheme for efficiently profiling paths in programs.
InvCop uses a combination of static and dynamic analysis to find violations of object invariants.
Darwin uses symbolic execution to root cause a test failure which used to pass in a prior version.
Netra is a static analysis tool to analyze access control configuration information. It can be used to identify potential vulnerabilities at the level of configuration metadata.

Recent Publications

Arun Chaganty, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani, Combining Relational Learning with SMT Solvers using CEGAR, in Computer Aided Verification (CAV), Lecture Notes in Computer Science, July 2013
Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, and Aditya V. Nori, Verification as Learning Geometric Concepts, in Static Analysis Symposium (SAS), Springer Verlag, June 2013
Venkatesh-Prasad Ranganath and Jithin Thomas, Structural and Temporal Patterns-Based Features, in Proceedings of International Workshop on Data Analysis Patterns in Software Engineering (DAPSE) 2013, ACM, 21 May 2013
Arun T. Chaganty, Aditya V. Nori, and Sriram K. Rajamani, Efficiently Sampling Probabilistic Programs via Program Analysis, in Artificial Intelligence and Statistics (AISTATS), April 2013
Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, and Aditya V. Nori, A Data Driven Approach for Algebraic Loop Invariants, in European Symposium on Programming (ESOP), Lecture Notes in Computer Science, March 2013
G Ramalingam and Kapil Vaswani, Fault Tolerance via Idempotence, in Principles of Programming Languages (POPL), ACM, January 2013
Andrew D. Gordon, Aditya V. Nori, and Sriram K. Rajamani, Probabilistic Inference Using Program Analysis, in Off the Beaten Track (OBT '13), January 2013
Michael Emmi, Akash Lal, and Shaz Qadeer, Asynchronous programs with prioritized task buffers, in Foundations of Software Engineering (FSE), November 2012
Ravichandhran Madhavan, Ganesan Ramalingam, and Kapil Vaswani, Modular Heap Analysis For Higher Order Programs, in Static Analysis Symposium (SAS), September 2012
Michael Emmi and Akash Lal, Finding Non-Terminating Executions in Distributed Asynchronous Programs, in Static Analysis Symposium (SAS), September 2012
Jose Faleiro, Sriram Rajamani, Kaushik Rajan, G Ramalingam, and Kapil Vaswani, Generalized Lattice Agreement, in Principles of Distributed Computing (PODC), ACM, July 2012
Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, and Akash Lal, Detecting Fair Non-Termination in Multithreaded Programs, in Computer-Aided Verification (CAV), July 2012
Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, in Computer-Aided Verification (CAV), July 2012
Rahul Sharma, Aditya V. Nori, and Alex Aiken, Interpolants as Classifiers, in Computer Aided Verification, Lecture Notes in Computer Science, July 2012
R. Manikantan, kaushik Rajan, and R. Govindarajan, Probabilistic Shared Cache Management(PriSM) , in ISCA, ACM/IEEE, June 2012
Aws Albarghouthi, Rahul Kumar, Aditya V. Nori, and Sriram K. Rajamani, Parallelizing Top-Down Interprocedural Analyses, in Programming Languages Design and Implementation (PLDI), ACM, June 2012
Moritz Y. Becker, Alessandra Russo, and Nik Sultana, Foundations of trust management, in IEEE Symposium on Security and Privacy, IEEE, 2012
Saurabh Joshi, Shuvendu Lahiri, and Akash Lal, Underspecified Harnesses and Interleaved Bugs, in Principles of Programming Languages (POPL) 2012, ACM SIGPLAN, January 2012
Bhargav S. Gulavani, Supratik Chakraborty, G. Ramalingam, and Aditya V. Nori, Bottom-up shape analysis using LISF, in Transactions on Programming Languages and Systems, ACM, November 2011
Dawei Qi, Abhik Roychoudhury, Zhengkai Liang, and Kapil Vaswani, DARWIN: An Approach for Debugging Evolving Programs, in ACM Transactions on Software Engineering and Methodology (TOSEM), ACM, August 2011
Kaushik Rajan, bill thies, and Abhishek Udupa, ALTER: Exploiting Breakable Dependences for Parallelization, in Proceedings of Programming Language Design and Implementation (PLDI 2011), Association for Computing Machinery, Inc., June 2011
Nels E. Beckman and Aditya V. Nori, Probabilistic, Modular and Scalable Inference of Typestate Specifications, in PLDI '11: Programming Languages Design and Implementation, Association for Computing Machinery, Inc., June 2011
R. Manikantan, Kaushik Rajan, and R. Govindarajan, NUcache: An Efficient Multicore Cache Organization Based on Next-Use Distance, in Proceedings of the International Conference on High Performance Computer Architecture (HPCA), 2011, IEEE, February 2011
R. Manikantan, Kaushik Rajan, and R. Govindarajan, Extended Histories: Improving Regularity and Performance in Correlation Prefetchers, in Proceedings of High Performance Embedded Architectures and Compilers, HIPEAC'2011, ACM, January 2011
Aditya Kanade, Rajeev Alur, Sriram Rajamani, and G Ramalingam, Representation Dependence Testing Using Program Inversion, in Foundations of Software Engineering (FSE), Association for Computing Machinery, Inc., November 2010

Click here for a full publication list

Alumni

Yamini Kannan <BITS Pilani, RSE, Berkeley>
Monu Kedia <IBM, RSE, IBM>
Krishna K. Mehra <IIT Kharagpur, RSE, Capillary Technologies>
Kanika Nema <IIT Bombay, RSE, VMWare>
Sai Deep Tetali <DAIICT, RSE, UCLA>
Aditya V. Thakur <IISc Bangalore, RSE, Wisconsin>
Abhishek Udupa <IISc Bangalore, RSE, UPenn>
Lakshmisubrahmanyam Velaga <IIT Kharagpur, RSE, IIM Bangalore>

Visitors

Gopalan Nandathur (Minnesota, 2010)
Anindya Banerjee (IMDEA, 2009)
Supratik Chakraborty (IIT Bombay, 2007)
Abhik Roychoudhury (NUS, 2008)
Stefan Schwoon (University of Stuttgart, 2006, 2007)
Prasad Sistla (University of Illinois, Chicago, 2006)

Interns

2010: Siddarth Agarwal (IIT Kanpur), Nels Beckman (CMU), Bharat Balasubramanian (UT Austin), Arun Chaganty (IIT Madras), Piyush Chawla (IIT Delhi), Neil Conway (Berkeley), Saurabh Joshi (IIT Kanpur), Abhishek Katyal (IIT Delhi), Nirmesh Malviya (IIT Kanpur), Hesam Samimi (UCLA), Rahul Srinivasan (IIT Bombay), Zachary Tatlock (UCSD)

2009: Jong-Hoon An (Maryland), Ashish Kumar Agarwal (IIT Kanpur), Vijay Victor D'Silva (Oxford University), William R. Harris (Wisconsin), Nicholas P. Johnson (Princeton), Vijay Anand Korthikanti (UIUC), Prakash J. Prabhu (Princeton), Rahul Sharma (IIT Delhi), Dheeraj Singh (IIT Kharagpur), Abhishek Udupa (IISc Bangalore), Shashank Yaduvanshi (IIT Delhi)

2008: Jyotirmoy Deshmukh (UT Austin), Bhargav S. Gulavani (IIT Bombay), Christopher Hayden (UMD), Michael Tschantz (CMU)

2007: Nels E. Beckman (CMU), Shilpa Bugde (SCIT, Pune), Pavol Cerny (UPenn), Pallavi Joshi (UC Berkeley), Akash Lal (Wisconsin), Robert J. Simmons (CMU), Christian Stefansen (DIKU), Pushkar Tripathi (IIT Delhi)

2006: Avik Chaudhuri (UC Santacruz), Prakash Chandrasekaran (CMI), Chris Conway (NYU), Madhu Gopinathan (IISc Bangalore), Bhargav S. Gulavani (IIT Bombay), Sumit Jha (CMU), Roman Manevich (Tel Aviv), and Kapil Vaswani (IISc Bangalore)

2005: Bhargav S. Gulavani (IIT Bombay), Aditya Parameswaran (IIT Bombay)

Careers

Microsoft Research India offers an unparalleled opportunity to conduct innovative and cutting-edge research and to see your research results improve the software used by most of the world. Microsoft Research’s agenda combines world-class research together with our academic colleagues and a unique opportunity to put ideas into practice by working with Microsoft product groups. Researchers at Microsoft Research have an unequalled opportunity to conduct fundamental research with few resource constraints, publish in leading academic conferences, and at the same time, influence and improve software development in the world’s largest software company and its customers.

We are still interviewing for researchers in the Rigorous Software Engineering group. You can apply here. If you know us from prior interactions, please send email to sriram@microsoft.com. We get a lot of email from people who do not really have a research background, so please be considerate of our time when you send email.

We welcome applicants from all over the world, regardless of nationality. India, and in particular Bangalore, is booming with fresh energy and opportunities! If you have ever considered living in India, or returning to live in India, now is the time to apply!

We are also looking for interns throughout the year. We are fairly flexible about when we can start and end internships. For internships, please apply here (Select the "Rigorous Software Engineering" group).