Skip to main content
SpringerLink
Log in

Software Model Checking: Searching for Computations in the Abstract or the Concrete

  • Conference paper
Integrated Formal Methods (IFM 2005)

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

Included in the following conference series:

Abstract

We review and discuss the current approaches to software model checking, including the complementary views of validation versus falsification and those of static versus dynamic analysis. For falsification, also known as bug finding, we advocate the need for blended approaches that combine the strengths of both static and dynamic analysis. We outline possible directions of research in this area.

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. Ball, T., Rajamani, S.: 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 

  2. Barrett, C., Berezin, S.: CVC lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating Test from Counterexamples. In: Proceedings of ICSE 2004 (26th International Conference on Software Engineering), May 2004. ACM, New York (2004)

    Google Scholar 

  4. Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proceedings of ISSTA 2002 (International Symposium on Software Testing and Analysis), pp. 123–133 (2002)

    Google Scholar 

  5. Cadar, C., Engler, D.: Execution Generated Test Cases: How to Make Systems Code Crash Itself. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 2–23. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Clarke, E., Kroening, 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)

    Chapter  Google Scholar 

  7. Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: Extracting Finite-State Models from Java Source Code. In: Proceedings of the 22nd International Conference on Software Engineering (2000)

    Google Scholar 

  8. Csallner, C., Smaragdakis, Y.: Check’n Crash: Combining Static Checking and Testing. In: Proceedings of ICSE 2005 (27th International Conference on Software Engineering), May 2005. ACM, New York (2005)

    Google Scholar 

  9. Dwyer, M.B., Hatcliff, J., Prasad, V.R., Robby: Exploiting Object Escape and Locking Information in Partial Order Reduction for Concurrent Object-Oriented Programs. In: Formal Methods in System Design (2004) (to appear)

    Google Scholar 

  10. Edvardsson, J.: A Survey on Automatic Test Data Generation. In: Proceedings of the 2nd Conference on Computer Science and Engineering, Linkoping, October 1999, pp. 21–28 (1999)

    Google Scholar 

  11. Ernst, M.D.: Static and dynamic analysis: synergy and duality. In: Proceedings of WODA 2003 (ICSE Workshop on Dynamic Analysis), Portland (May 2003)

    Google Scholar 

  12. Flanagan, C., Godefroid, P.: Dynamic Partial-Order Reduction for Model Checking Software. In: Proceedings of POPL 2005 (32nd ACM Symposium on Principles of Programming Languages), Long beach, January 2005, pp. 110–121 (2005)

    Google Scholar 

  13. Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems – An Approach to the State-Explosion Problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)

    Google Scholar 

  14. Godefroid, P.: Model Checking for Programming Languages using VeriSoft. In: Proceedings of POPL 1997 (24th ACM Symposium on Principles of Programming Languages), Paris, January 1997, pp. 174–186 (1997)

    Google Scholar 

  15. Godefroid, P.: The Soundness of Bugs is What Matters (Position Paper). In: Proceedings of BUGS 2005 (PLDI 2005 Workshop on the Evaluation of Software Defect Detection Tools), Chicago (June 2005)

    Google Scholar 

  16. Godefroid, P., Klarlund, N., Sen, K.: DART: Directed Automated Random Testing. In: Proceedings of PLDI 2005 (ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation), Chicago, June 2005, pp. 213–223 (2005)

    Google Scholar 

  17. Graf, S., Saidi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Google Scholar 

  18. Gunter, E., Peled, D.: Path Exploration Tool. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 405. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Gupta, N., Mathur, A.P., Soffa, M.L.: Generating test data for branch coverage. In: Proceedings of the 15th IEEE International Conference on Automated Software Engineering, September 2000, pp. 219–227 (2000)

    Google Scholar 

  20. Hastings, R., Joyce, B.: Purify: Fast Detection of Memory Leaks and Access Errors. In: Proceedings of the Usenix Winter 1992 Technical Conference, Berkeley, January 1992, pp. 125–138 (1992)

    Google Scholar 

  21. Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, Portland, January 2002, pp. 58–70 (2002)

    Google Scholar 

  22. Holzmann, G.J., Smith, M.H.: A Practical Method for Verifying Event-Driven Software. In: Proceedings of the 21st International Conference on Software Engineering, pp. 597–607 (1999)

    Google Scholar 

  23. Ics. web page, http://www.icansolve.com/

  24. King, J.C.: Symbolic Execution and Program Testing. Journal of the ACM 19(7), 385–394 (1976)

    Article  MATH  Google Scholar 

  25. Korel, B.: A dynamic Approach of Test Data Generation. In: IEEE Conference on Software Maintenance, San Diego, November 1990, pp. 311–317 (1990)

    Google Scholar 

  26. Larson, E., Austin, T.: High Coverage Detection of Input-Related Security Faults. In: Proceedings of 12th USENIX Security Symposium, D.C (August 2003)

    Google Scholar 

  27. lp_solve. web page, http://groups.yahoo.com/group/lp_solve/

  28. Musuvathi, M., Park, D., Chou, A., Engler, D., Dill, D.: CMC: A pragmatic approach to model checking real code. In: Proceedings of OSDI 2002 (2002)

    Google Scholar 

  29. Myers, G.J.: The Art of Software Testing. Wiley, Chichester (1979)

    Google Scholar 

  30. Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-Safe Retrofitting of Legacy Code. In: Proceedings of POPL 2002 (29th ACM Symposium on Principles of Programming Languages), Portland, January 2002, pp. 128–139 (2002)

    Google Scholar 

  31. Offutt, J., Hayes, J.: A Semantic Model of Program Faults. In: Proceedings of ISSTA 1996 (International Symposium on Software Testing and Analysis), San Diego, January 1996, pp. 195–200 (1996)

    Google Scholar 

  32. Pasareanu, C., Pelanek, R., Visser, W.: Concrete Model Checking with Abstract Matching and Refinement. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 52–66. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  33. Qadeer, S., Wu, D.: KISS: Keep It Simple and Sequential. In: Proceedings of PLDI 2004 (ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation), Washington D.C (June 2004)

    Google Scholar 

  34. Sen, K., Marinov, D., Agha, G.: CUTE: A Concolic Unit testing Engine for C. In: Proceedings of FSE 2005 (13th International Symposium on the Foundations of Software Engineering), Lisbon (September 2005)

    Google Scholar 

  35. Simplify. web page, http://research.compaq.com/SRC/esc/Simplify.html

  36. Tip, F.: A survey of program slicing techniques. Journal of Programming Languages 3(3), 121–189 (1995)

    Google Scholar 

  37. Valgrind. web page, http://valgrind.org/

  38. Visser, W., Havelund, K., Brat, G., Park, S.: Model Checking Programs. In: Proceedings of ASE 2000 (15th International Conference on Automated Software Engineering), Grenoble (September 2000)

    Google Scholar 

  39. Visser, W., Pasareanu, C., Khurshid, S.: Test Input Generation with Java PathFinder. In: Proceedings of ACM SIGSOFT ISSTA 2004 (International Symposium on Software Testing and Analysis), Boston (July 2004)

    Google Scholar 

  40. Xie, T., Marinov, D., Schulte, W., Notkin, D.: Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. TACAS 2005, pp. 365–381. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Bell Laboratories, Lucent Technologies,  

    Patrice Godefroid

  2. Google,  

    Nils Klarlund

Authors
  1. Patrice Godefroid
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nils Klarlund
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Mathematics and Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600, Eindhoven, MB, The Netherlands

    Judi Romijn

  2. School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Australia

    Graeme Smith

  3. Formal Methods and Tools, Department of Computer Science, University of Twente, P.O. Box 217, 7500AE, Enschede, The Netherlands

    Jaco van de Pol

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Godefroid, P., Klarlund, N. (2005). Software Model Checking: Searching for Computations in the Abstract or the Concrete. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_3

Download citation

  • DOI: https://doi.org/10.1007/11589976_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-30492-0

  • Online ISBN: 978-3-540-32240-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation