Abstract
Stanse is a free (available under the GPLv2 license) modular framework for finding bugs in C programs using static analysis. Its two main design goals are 1) ability to process large software projects like the Linux kernel and 2) extensibility with new bug-finding techniques with a minimal effort. Currently there are four bug-finding algorithms implemented within Stanse: AutomatonChecker checks properties described in an automata-based formalism, ThreadChecker detects deadlocks among multiple threads, LockChecker finds locking errors based on statistics, and ReachabilityChecker looks for unreachable code. Stanse has been tested on the Linux kernel, where it has found dozens of previously undiscovered bugs.
This is a preview of subscription content, log in via an institution to check access.
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
Chou, A., Chelf, B., Engler, D., Heinrich, M.: Using meta-level compilation to check FLASH protocol code. ACM SIGOPS Oper. Syst. Rev. 34(5), 59–70 (2000)
Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: OSDI 2000, pp. 1–16 (2000)
Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: A general approach to inferring errors in systems code. ACM SIGOPS Oper. Syst. Rev. 35(5), 57–72 (2001)
Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: PLDI 2002, pp. 69–82. ACM (2002)
Hovemeyer, D., Pugh, W.: Finding bugs is easy. In: OOPSLA 2004, pp. 132–136. ACM (2004)
Shapiro, M., Horwitz, S.: Fast and accurate flow-insensitive points-to analysis. In: POPL 1997, pp. 1–14. ACM (1997)
Steensgaard, B.: Points-to analysis in almost linear time. In: POPL 1996, pp. 32–41. ACM (1996)
Voung, J.W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: ESEC-FSE 2007, pp. 205–214. ACM (2007)
Coverity, http://www.coverity.com/products/
FindBugs, http://findbugs.sourceforge.net/
Klocwork, http://www.klocwork.com/products/
Smatch, http://smatch.sourceforge.net/
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
Obdržálek, J., Slabý, J., Trtík, M. (2012). STANSE: Bug-Finding Framework for C Programs. In: Kotásek, Z., Bouda, J., Černá, I., Sekanina, L., Vojnar, T., Antoš, D. (eds) Mathematical and Engineering Methods in Computer Science. MEMICS 2011. Lecture Notes in Computer Science, vol 7119. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25929-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-25929-6_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25928-9
Online ISBN: 978-3-642-25929-6
eBook Packages: Computer ScienceComputer Science (R0)