Advertisement

Towards an Open Framework for C Verification Tools Benchmarking

  • Alexey Khoroshilov
  • Vadim Mutilin
  • Eugene Novikov
  • Pavel Shved
  • Alexander Strakh
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7162)

Abstract

The paper presents a twofold verification system that aimes to be an open platform for experimentation with various verification techniques as well as an industrial-ready domain specific verification tool for Linux device drivers. We describe the architecture of the verification system and discuss a perspective to build an open benchmarking suite on top of it.

Keywords

verification tools benchmarking static analysis device driver verification domain specific verification reachability verification aspect-oriented programming 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
  2. 2.
    Web-site: Klocwork insight, http://www.klocwork.com/products/insight/
  3. 3.
    Nesov, V.: Automatically finding bugs in open source programs. In: Third International Workshop on Foundations and Techniques for Open Source Software Certification. OpenCert 2009, vol. 20, pp. 19–29 (2009)Google Scholar
  4. 4.
    Dillig, I., Dillig, T., Aiken, A.: Sound, complete and scalable path-sensitive analysis. SIGPLAN Not. 43, 270–280 (2008)CrossRefGoogle Scholar
  5. 5.
    Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39, 92–106 (2004)CrossRefGoogle Scholar
  6. 6.
    Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Softw. 19, 42–51 (2002)CrossRefGoogle Scholar
  7. 7.
    Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: Formal Methods in Computer Aided Design (2010)Google Scholar
  8. 8.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast: Applications to software engineering. Int. J. Softw. Tools Technol. Transf. 9(5), 505–525 (2007)CrossRefGoogle Scholar
  9. 9.
    Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. Technical report, School of Computing Science, Simon Fraser University (2009)Google Scholar
  10. 10.
    Clarke, E., Kroning, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The Static Driver Verifier Research Platform. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 119–122. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Khoroshilov, A., Mutilin, V.: Formal methods for open source components certification. In: 2nd International Workshop on Foundations and Techniques for Open Source Software Certification. OpenCert 2008, pp. 52–63 (2008)Google Scholar
  14. 14.
    Khoroshilov, A., Mutilin, V., Shcherbina, V., Strikov, O., Vinogradov, S., Zakharov, V.: How to cook an automated system for Linux driver verification. In: 2nd Spring Young Researchers’ Colloquium on Software Engineering. SYRCoSE 2008, vol. 2, pp. 11–14 (2008)Google Scholar
  15. 15.
    Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing Linux Driver Verification Process. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 165–176. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  16. 16.
    Kroah-Hartman, G., Corbet, J., McPherson, A.: Linux kernel development: How fast it is going, who is doing it, what they are doing, and who is sponsoring it (2010), http://www.linuxfoundation.org/docs/lf_linux_kernel_development_2010.pdf
  17. 17.
    Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: SOSP 2001: Proceedings of the Eighteenth ACM Symposium on Operating Systems Principles, pp. 73–88. ACM, New York (2001)CrossRefGoogle Scholar
  18. 18.
    Swift, M.M., Bershad, B.N., Levy, H.M.: Improving the reliability of commodity operating systems. In: SOSP 2003: Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles, pp. 207–222. ACM, New York (2003)CrossRefGoogle Scholar
  19. 19.
    Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking. Technical report, Microsoft Research (2001)Google Scholar
  20. 20.
    Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: Proceedings of the 2008 International Symposium on Software Testing and Analysis, ISSTA 2008, pp. 3–14. ACM, New York (2008)CrossRefGoogle Scholar
  21. 21.
    Post, H., Küchlin, W.: Integrated Static Analysis for Linux Device Driver Verification. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 518–537. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  22. 22.
    Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: ASE 2007: Proceedings of the Twenty-Second IEEE/ACM International Conference on Automated Software Engineering, pp. 501–504. ACM, New York (2007)CrossRefGoogle Scholar
  23. 23.
    Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-Based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  24. 24.
    Post, H., Küchlin, W.: Automatic data environment construction for static device drivers analysis. In: Proceedings of the 2006 Conference on Specification and Verification of Component-Based Systems, SAVCBS 2006, pp. 89–92. ACM, New York (2006)CrossRefGoogle Scholar
  25. 25.
    Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  26. 26.
    Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 25–32 (November 2009)Google Scholar
  27. 27.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction Refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  28. 28.
    Weide, B.W., Sitaraman, M., Harton, H.K., Adcock, B., Bucci, P., Bronish, D., Heym, W.D., Kirschenbaum, J., Frazier, D.: Incremental Benchmarks for Software Verification Tools and Techniques. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 84–98. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  29. 29.
    Web-site: Problems found in Linux kernels, http://linuxtesting.org/results/ldv

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Alexey Khoroshilov
    • 1
  • Vadim Mutilin
    • 1
  • Eugene Novikov
    • 1
  • Pavel Shved
    • 1
  • Alexander Strakh
    • 1
  1. 1.Institute for System ProgrammingRussian Academy of SciencesRussia

Personalised recommendations