2009 | OriginalPaper | Buchkapitel
The Yogi Project: Software Property Checking via Static Analysis and Testing
verfasst von : Aditya V. Nori, Sriram K. Rajamani, SaiDeep Tetali, Aditya V. Thakur
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.