The Yogi Project: Software Property Checking via Static Analysis and Testing

PLDI 2012 Tutorial

Saturday, June 16, 2012, Beijing, China

Tutorial Slides

Introduction

Static analysis and testing have always had complementary strengths and weaknesses. With static analysis, we can obtain very good coverage and analyze program paths that are hard to exercise using testing, but we are forced to deal with scalability issues and false errors. With runtime testing, we can obtain only partial coverage, but the approach scales to large programs and every error that is reported is indeed realizable. Thus, attempting to combine the complementary strengths of static analysis and runtime testing is natural. For the past few years, we have been investigating methods for combining static analysis in the style of counter-example driven refinement ala SLAM, with runtime testing and automatic test case generation approaches in the style of concolic execution ala DART. Our first attempt in this direction was the Synergy algorithm [8], which handled single procedure programs with only integer variables. Then, we proposed the Dash algorithm [7], which had new ideas to handle pointer aliasing and procedure calls in programs. Subsequently, we proposed the Smash algorithm [4] that computes may and must information compositionally and also explains the analysis in the large and diverse amount of existing work in the area. More recently, we proposed the Bolt algorithm [1] that uses MapReduce style parallelism to scale up top-down interprocedural analyses. Throughout this evolution, Yogi has been our implementation vehicle to realize and evaluate these algorithms. We have spent over 4 person-years of engineering [5] to make the tool robust and usable. At this point, Yogi has been run over several hundreds of thousands of lines of C code – in particular, it is now routinely used to verify and test several properties of Windows 7 device drivers. In this tutorial, we will present a detailed account of the evolution of Yogi (http://research.microsoft.com/yogi ) and our experiences engineering this tool.

Objective

Though several verification tools are finding industrial use, the “secret sauce” that makes them scalable and usable is not widely known. The main objective of this tutorial is to give researchers a comprehensive picture of what it takes to design and engineer an industrial strength property checking engine. In particular, we will give:

  • A comprehensive treatment of Yogi’s main algorithms Synergy, Dash, Smash and Bolt their evolution.
  • Various details of how the various algorithms in the tool have been implemented.
  • A description of all the optimizations built into Yogi which enables the tool to scale and work on industrial strength applications.
  •  Extensive demos that illustrate points 1, 2 and 3. We also plan to make Yogi available for download around March 2012.

Description of Yogi

A detailed description of Yogi's algorithms can be found in [7, 6, 3, 2, 1]. The goal of Yogi is to solve the property checking problem. An instance of the property checking problem consists of a sequential program P and an assertion . An answer to the property checking problem is pass if every run of P satisfies the property . The answer is fail if there exists some run of P that violates .

Static analysis and testing are complementary approaches to the property checking problem. With static analysis, we can obtain very good coverage and analyze program paths that are hard to exercise using testing, but we are forced to deal with scalability issues and false errors. With runtime testing, we can obtain only partial coverage, but the approach scales to large programs and every error that is reported is indeed realizable.

One of the unique features of Yogi is that it simultaneously searches for both a test to establish that the program violates the property, and an abstraction to establish that the program satisfies the property. If the abstraction has a path that leads to the violation of the property, Yogi attempts to focus test case generation along that path. If such a test case cannot be generated, Yogi uses information from the unsatisfiable constraint from the test case generator to refine the abstraction. Thus, the construction of test cases and abstraction proceed hand-in-hand, using error traces in the abstraction to guide test case generation, and constraints from failed test-case generation attempts to guide refinement of the abstraction.

We have engineered Yogi in such a way that it plugs into Microsoft's Static Driver Verifier (SDV) framework. We have used this framework to run Yogi on several Windows 7 device drivers and properties.

Topics covered

  •  Overview of the current state-of-the-art in property checking – software model checking tools and testing tools.
  •  Description of the Synergy, Dash, Smash and Bolt algorithms.
  •  Architecture of Yogi and integration with Microsoft’s Static Driver Verifier (SDV) toolkit.
  •  Engineering optimizations in Yogi – details on what works and what does not work.

Target audience

The target audience includes faculty, graduate students and undergraduate students and anybody who is concerned about software reliability and program correctness.

About the Presenters

Aditya V. Nori is a researcher at Microsoft Research India. His research interests include algorithms for the analysis of programs and machine learning with special focus on tools for improving software reliability and programmer productivity. He received his PhD from the Indian Institute of Science, Bangalore in 2005.
Sriram K. Rajamani is the assistant managing director of Microsoft Research India. His research interests are in programming languages and programming tools. Several of his projects have had influence in both academia and industry, the most notable one being the SLAM project, which is the basis for Microsoft's Static Driver Verifier. He received his PhD from the University of California at Berkeley in 1999.

References

[1] 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

[2] Aditya V. Nori and Sriram K. Rajamani, An Empirical Study of Optimizations in Yogi, in ICSE '10: International Conference on Software Engineering, May 2010

[3] 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

[4] 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

[5] 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

[6] 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

[7] 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

[8] 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