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

Nori, Aditya V. and Rajamani, Sriram K. and Tetali, SaiDeep and Thakur, Aditya V.
15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2009

We present Yogi, a tool that checks properties of C programs by combining static analysis and testing. Yogi implements the Dash algorithm which performs verification by combining directed testing and abstraction. We have engineered Yogi in such a way that it plugs into Microsoft’s Static Driver Verifier framework. We have used this framework to run Yogi on 69 Windows Vista drivers with 85 properties. We find that the new algorithm enables Yogi to scale much better than Slam, which is the current engine driving Microsoft’s Static Driver Verifier.

PDF     Springer©    

@inproceedings{nori_etal_TACAS09,
  author = {Nori, Aditya V. and Rajamani, Sriram K. and Tetali, SaiDeep and Thakur, Aditya V.},
  title = {The Yogi Project: Software Property Checking via Static
                    Analysis and Testing},
  booktitle = {15th International Conference on Tools and Algorithms
                    for the Construction and Analysis of Systems (TACAS)},
  year = {2009},
  pages = {178--181},
  doi = {10.1007/978-3-642-00768-2_17},
  publisher = {Springer}
}