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.
We are working on static analysis and testing to find bugs in programs and also guarantee certain properties about programs: Yogi.
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.
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
- 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.
- 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
- 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>
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)
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)
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 firstname.lastname@example.org. 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).
- Bayez accepted at CAV'13!
- Verification as Learning Geometric Concepts accepted at SAS'13!
- Two papers (Probabilistic Programming and Fault Tolerance via Idempotence) at POPL'13!
- Generalized Lattice Agreement accepted at PODC'12!
- Three papers accepted at CAV'12: Corral, Mutant, and Interpolants as Classifiers!
- Tom Ball and Sriram Rajamani are receipients of the 2011 CAV award!!!
- Automatic Predicate Abstraction of C Programs wins the Most Influential PLDI Paper award!