The Yogi Project
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 synergy of testing and static analysis can be harnessed to efficiently validate software.
People
MSR colleagues
- B. Ashok (Bash)
Windows colleagues
- Rahul Kumar
- Vladimir Levin
- Jakob Lichtenberg
Collaborators
- Supratik Chakraborty (IIT Bombay)
- Patrice Godefroid (MSR Redmond)
- Thomas A. Henzinger (EPFL)
- Akash Lal (MSR India)
Interns
- 2011: Aws Albarghouthi (UToronto)
- 2010: Abhishek Katyal (IIT Delhi), Rahul Sharma (Btech thesis, IIT Delhi), Zachary Tatlock (UCSD)
- 2009: Vijay Victor D'Silva (Oxford University), William Harris (Wisconsin), Sai Deep Tetali (UCLA)
- 2008: Bhargav S. Gulavani (IIT Bombay), Aditya Thakur (Wisconsin)
- 2007: Nels E. Beckman (CMU), Robert J. Simmons (CMU)
- 2006: Bhargav S. Gulavani (IIT Bombay), Yamini Kannan (UC Berkeley)
Publications
- Aws Albarghouthi, Rahul Kumar, Aditya V. Nori and Sriram K. Rajamani, Parallelizing Top-down Interprocedural Analyses, in PLDI '12: Programming Languages Design and Implementation, June 2012
- William R. Harris, Akash Lal, Aditya V. Nori and Sriram K. Rajamani, Alternation for Termination, in SAS '10: Static Analysis Symposium, September 2010
- Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, and Sriram K. Rajamani, Refining Abstract Interpretations, in Information Processing Letters, May 2010
- Aditya V. Nori and Sriram K. Rajamani, An Empirical Study of Optimizations in Yogi, in ICSE '10: International Conference on Software Engineering, May 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, February 2010
- Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and Sai Deep Tetali, Compositional May-Must Program Analysis: Unleashing the Power of Alternation, in Principles of Programming Languages (POPL), January 2010
- Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali, Aditya V. Thakur, The Yogi Project: Software Property Checking via Static Analysis and Testing, in TACAS '09: Tools and Algorithms for the Construction and Analysis of Systems, March 2009
- Patrice Godefroid, Peli de Halleux, Michael Y. Levin, Aditya V. Nori, Sriram K. Rajamani, Wolfram Schulte, Nikolai Tillmann, Automated Software Testing Using Program Analysis, in IEEE Software: Special Issue on Software Development Tools, October 2008
- Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Proofs from Tests, in ISSTA '08: International Symposium on Software Testing and Analysis, July 2008
- Bhargav S. Gulavani, Supratik Chakraborty, Aditya V. Nori, Sriram K. Rajamani, Automatically Refining Abstract Interpretations, in TACAS '08: Tools and Algorithms for the Construction and Analysis of Systems, March 2008
- Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, Sriram K. Rajamani, Synergy: A New Algorithm for Property Checking, in FSE '06: Foundations of Software Engineering (ACM SIGSOFT Distinguished Paper) , November 2006
Presentations
- Yogi PLDI 2012 Tutorial
- An Empirical Study of Optimizations in Yogi (ICSE 2010)
- Compositional May-Must Program Analysis: Unleashing the Power of Alternation (POPL 2010)
- The Yogi Project: Software Property Checking via Static Analysis and Testing (TACAS 2009)
- Proofs from Tests (ISSTA 2008)
- Synergy: A New Algorithm for Property Checking (FSE 2006)
Contact
Please send inquiries about the Yogi project to adityan [AT] microsoft.com or sriram[AT] microsoft.com
