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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Web-site: Coverity, http://www.coverity.com/products/static-analysis.html
Web-site: Klocwork insight, http://www.klocwork.com/products/insight/
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)
Dillig, I., Dillig, T., Aiken, A.: Sound, complete and scalable path-sensitive analysis. SIGPLAN Not. 43, 270–280 (2008)
Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39, 92–106 (2004)
Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Softw. 19, 42–51 (2002)
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)
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)
Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. Technical report, School of Computing Science, Simon Fraser University (2009)
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)
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)
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)
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)
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)
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)
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
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)
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)
Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking. Technical report, Microsoft Research (2001)
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)
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)
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)
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)
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)
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)
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)
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)
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)
Web-site: Problems found in Linux kernels, http://linuxtesting.org/results/ldv
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Khoroshilov, A., Mutilin, V., Novikov, E., Shved, P., Strakh, A. (2012). Towards an Open Framework for C Verification Tools Benchmarking. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2011. Lecture Notes in Computer Science, vol 7162. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29709-0_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-29709-0_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29708-3
Online ISBN: 978-3-642-29709-0
eBook Packages: Computer ScienceComputer Science (R0)