The Yogi Project: Software Property Checking via Static Analysis and Testing. 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.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Ponzio, Pablo; Godio, Ariel; Rosner, Nicolás; Arroyo, Marcelo; Aguirre, Nazareno; Frias, Marcelo F.: Efficient bounded model checking of heap-manipulating programs using tight field bounds (2021)
  2. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  3. Jhala, Ranjit; Podelski, Andreas; Rybalchenko, Andrey: Predicate abstraction for program verification (2018)
  4. McMillan, Kenneth L.: Interpolation and model checking (2018)
  5. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)
  6. Sharma, Rahul; Nori, Aditya V.; Aiken, Alex: Bias-variance tradeoffs in program analysis (2014)
  7. Cousot, Patrick; Cousot, Radhia; Fähndrich, Manuel; Logozzo, Francesco: Automatic inference of necessary preconditions (2013) ioport
  8. Sharma, Rahul; Gupta, Saurabh; Hariharan, Bharath; Aiken, Alex; Liang, Percy; Nori, Aditya V.: A data driven approach for algebraic loop invariants (2013)
  9. Bjørner, Nikolaj: Taking satisfiability to the next level with Z3 (abstract) (2012)
  10. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: Collaborative verification and testing with explicit assumptions (2012)
  11. Jaffar, Joxan; Murali, Vijayaraghavan; Navas, Jorge A.; Santosa, Andrew E.: TRACER: a symbolic execution tool for verification (2012)
  12. Obdržálek, Jan; Trtík, Marek: Efficient loop navigation for symbolic execution (2011)
  13. Godefroid, Patrice; Nori, Aditya V.; Rajamani, Sriram K.; Tetali, Sai Deep: Compositional may-must program analysis: unleashing the power of alternation (2010)
  14. Nori, Aditya V.; Rajamani, Sriram K.; Tetali, SaiDeep; Thakur, Aditya V.: The Yogi project: software property checking via static analysis and testing (2009) ioport