Skip to main content
SpringerLink
Log in

SMT-Based False Positive Elimination in Static Program Analysis

  • Conference paper
Formal Methods and Software Engineering (ICFEM 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7635))

Included in the following conference series:

Abstract

Static program analysis for bug detection in large C/C++ projects typically uses a high-level abstraction of the original program under investigation. As a result, so-called false positives are often inevitable, i.e., warnings that are not true bugs. In this work we present a novel abstraction refinement approach to automatically investigate and eliminate such false positives. Central to our approach is to view static analysis as a model checking problem, to iteratively compute infeasible sub-paths of infeasible paths using SMT solvers, and to refine our models by adding observer automata to exclude such paths. Based on this new framework we present an implementation of the approach into the static analyzer Goanna and discuss a number of real-life experiments on larger C code projects, demonstrating that we were able to remove most false positives automatically.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Armando, A., Mantovani, J., Platania, L.: Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. Int. J. Softw. Tools Techn. Transf. 11(1), 69–83 (2009)

    Article  Google Scholar 

  2. Balakrishnan, G., Sankaranarayanan, S., Ivančić, F., Wei, O., Gupta, A.: SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 238–254. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.: Automatic Predicate Abstraction of C Programs. In: Proc. 2001 ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI 2001), pp. 203–213. ACM (2001)

    Google Scholar 

  4. Ball, T., Rajamani, S.K.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Burstall, R.: Some Techniques for Proving Correctness of Programs which Alter Data Structures. Mach. Intell. 7, 23–50 (1972)

    MATH  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-Based Bounded Model Checking for Embedded ANSI-C Software. In: Proc. 24th IEEE/ACM Int. Conf. Automated Software Engineering (ASE 2009), pp. 137–148. IEEE (2009)

    Google Scholar 

  8. Dams, D.R., Namjoshi, K.S.: Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 138–160. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. de la Banda, M., Stuckey, P., Wazny, J.: Finding All Minimal Unsatisfiable Subsets. In: 5th Int. ACM SIGPLAN Conf. Principles and Practice of Declarative Programming (PPDP 2003), pp. 32–43. ACM (2003)

    Google Scholar 

  10. de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Delahaye, M., Botella, B., Gotlieb, A.: Explanation-Based Generalization of Infeasible Path. In: Proc. 3rd Int. Conf. Software Testing, Verification and Validation (ICST 2010), pp. 215–224. IEEE (2010)

    Google Scholar 

  12. D’Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. CAD Integ. Circ. Syst. 27(7), 1165–1178 (2008)

    Article  Google Scholar 

  13. Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., Rauch, F.: Model Checking Software at Compile Time. In: Proc. 1st Joint IEEE/IFIP Symp. Theoretical Aspects of Software Engineering (TASE 2007), pp. 45–56. IEEE (2007)

    Google Scholar 

  14. Fehnker, A., Huuck, R., Seefried, S.: Counterexample Guided Path Reduction for Static Program Analysis. In: Dams, D., Hannemann, U., Steffen, M. (eds.) Concurrency, Compositionality, and Correctness. LNCS, vol. 5930, pp. 322–341. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Fehnker, A., Huuck, R., Seefried, S., Tapp, M.: Fade to Grey: Tuning Static Program Analysis. In: Proc. 3rd Int. Wsh. Harnessing Theories for Tool Support in Software (TTSS 2009), pp. 38–51. UNU-IIST (2009)

    Google Scholar 

  16. Harris, W.R., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Program Analysis via Satisfiability Modulo Path Programs. In: Proc. 37th ACM SIGPLAN-SICACT Symp. Principles of Programming Languages (POPL 2010), pp. 71–82. ACM (2010)

    Google Scholar 

  17. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Holzmann, G.J.: Static Source Code Checking for User-Defined Properties. In: Proc. 6th World Conf. Integrated Design and Process Technology (IDPT 2002). SDPS (2002)

    Google Scholar 

  19. Huuck, R., Fehnker, A., Seefried, S., Brauer, J.: Goanna: Syntactic Software Model Checking. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 216–221. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  20. ISO/IEC. ISO/IEC 9899:2011 Information Technology – Programming Languages – C. ISO, Genève (2011)

    Google Scholar 

  21. Junker, M.: Using SMT Solvers for False Positive Elimination in Static Program Analysis. Master’s thesis, Universität Augsburg (2010), http://www4.in.tum.de/~junkerm/publications/thesis.pdf

  22. Liffiton, M.H., Sakallah, K.A.: On Finding All Minimally Unsatisfiable Subformulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 173–186. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  23. Okun, V., Delaitre, A., Black, P.E. (eds.): Report on the Third Static Analysis Tool Exposition (SATE 2010). SP-500-283, U.S. Nat. Inst. Stand. Techn. (2011)

    Google Scholar 

  24. Schmidt, D.A., Steffen, B.: Program Analysis as Model Checking of Abstract Interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  25. Stump, A., Barrett, C., Dill, D., Levitt, J.: A Decision Procedure for an Extensional Theory of Arrays. In: Proc. 16th Ann. IEEE Symp. Logic in Computer Science (LICS 2001), pp. 29–37. IEEE (2001)

    Google Scholar 

  26. Yang, Z., Al-Rawi, B., Sakallah, K., Huang, X., Smolka, S., Grosu, R.: Dynamic Path Reduction for Software Model Checking. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 322–336. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Technische Universität München, Munich, Germany

    Maximilian Junker

  2. NICTA, University of New South Wales, Sydney, Australia

    Ralf Huuck & Ansgar Fehnker

  3. Universität Augsburg, Augsburg, Germany

    Alexander Knapp

Authors
  1. Maximilian Junker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ralf Huuck
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ansgar Fehnker
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alexander Knapp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Japan Advanced Institute of Science and Technology (JAIST), 1-1, Asahidai, 923-1292, Nuomi, Ishikawa, Japan

    Toshiaki Aoki

  2. National Institute of Advanced Industrial Science and Technology (AIST), Nakoji 3-11-46, 661-0974, Amagasaki, Hyogo, Japan

    Kenji Taguchi

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Junker, M., Huuck, R., Fehnker, A., Knapp, A. (2012). SMT-Based False Positive Elimination in Static Program Analysis. In: Aoki, T., Taguchi, K. (eds) Formal Methods and Software Engineering. ICFEM 2012. Lecture Notes in Computer Science, vol 7635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34281-3_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34281-3_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34280-6

  • Online ISBN: 978-3-642-34281-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation