Videos

Projects

Publications

People

Downloads

Our Research

Connections

Careers

Hub

Researcher Reflections

Stretch into the Unknown

> Groups > Rigorous Software Engineering

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, Poirot.

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
Poirot: The concurrency sleuth
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

Rahul Sharma, Aditya V. Nori, and Alex Aiken, Interpolants as Classifiers, in Computer Aided Verification, Lecture Notes in Computer Science, July 2012
Akash Lal, Shaz Qadeer, and Shuvendu Lahiri, Corral: A Solver for Reachability Modulo Theories, in Computer-Aided Verification (CAV), 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
Jose Faleiro, Sriram Rajamani, Kaushik Rajan, G Ramalingam, and Kapil Vaswani, Generalized Lattice Agreement, in Proceedings of Symposium on Principles of Distributed Computing (PODC), ACM, 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
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
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
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
Shuvendu K. Lahiri, Kapil Vaswani, and Tony Hoare, Differential Static Analysis: Opportunities, Applications, and Challenges, in 2010 FSE/SDP Workshop on the Future of Software Engineering Research (Position paper) , Association for Computing Machinery, Inc., November 2010
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
William R. Harris, Akash Lal, Aditya V. Nori, and Sriram K. Rajamani, Alternation for Termination, in SAS '10: Static Analysis Symposium, Springer Verlag, September 2010
Kaushik Rajan, Sriram Rajamani, and Shashank Yaduvanshi, GUESSTIMATE: A Programming Model for Collaborative Distributed Systems, in Proceedings of Programming Language Design and Implementation (PLDI 2010), Association for Computing Machinery, Inc., June 2010
Prakash Prabhu, G Ramalingam, and Kapil Vaswani, Safe Programmable Speculative Parallelism, in Proceedings of Programming Language Design and Implementation (PLDI), Association for Computing Machinery, Inc., June 2010
Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, and Sriram K. Rajamani, Refining Abstract Interpretations, in Information Processing Letters, Elsevier , May 2010
Aditya V. Nori and Sriram K. Rajamani, An Empirical Study of Optimizations in Yogi, in International Conference on Software Engineering (ICSE), Association for Computing Machinery, Inc., May 2010
Jyotirmoy Deshmukh, G. Ramalingam, Venkatesh Prasad Ranganath, and Kapil Vaswani, Logical Concurrency Control From Sequential Proofs, in Proceedings of European Symposium on Programming (ESOP) - ETAPS Best Paper, March 2010
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, and Aditya V. Thakur, Proofs from Tests, in IEEE Transactions on Software Engineering (special issue on the ISSTA 2008 best papers), IEEE, March 2010
Sandya Mannarswamy, Dhruva Chakrabarti, Kaushik Rajan, and Sujoy Saraswati, Compiler Aided Selective Lock Assignment for Improving the Performance of Software Transactional Memory, in Proceedings of Principles and Practice of Parallel Programming (PPoPP 2010), Association for Computing Machinery, Inc., January 2010
Hagit Attiya, Ganesan Ramalingam, and Noam Rinetzky, Sequential Verification of Serializability, in Principles of Programming Languages (POPL), Association for Computing Machinery, Inc., January 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).