Skip to main content
SpringerLink
Log in

Combining Static and Dynamic Reasoning for the Discovery of Program Properties

  • Conference paper
Book cover Model Checking Software (SPIN 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5156))

Included in the following conference series:

  • 493 Accesses

Abstract

Combinations of static and dynamic analyses can be profitably employed in tasks such as program understanding, bug detection, behavior discovery, etc. In the past several years, we have explored a particular scheme for improving the quality of bug reports in a sequence of tools: JCrasher, Check ’n’ Crash, and DSD-Crasher. We have additionally explored the combination of dynamic and symbolic execution for the purpose of inferring program invariants in the DySy tool. In this talk, we discuss such approaches, while distinguishing the conceptual benefits and drawbacks of each approach from the abilities and shortcomings of the current representative tools.

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

References

  1. Csallner, C., Smaragdakis, Y.: JCrasher: An automatic robustness tester for Java. Software—Practice & Experience 34(11), 1025–1050 (2004)

    Article  Google Scholar 

  2. Csallner, C., Smaragdakis, Y.: Check ’n’ Crash: Combining static checking and testing. In: Proc. 27th International Conference on Software Engineering (ICSE), May 2005, pp. 422–431. ACM, New York (2005)

    Chapter  Google Scholar 

  3. Csallner, C., Smaragdakis, Y.: DSD-Crasher: A hybrid analysis tool for bug finding. In: Proc. ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), July 2006, pp. 245–254. ACM, New York (2006)

    Google Scholar 

  4. Csallner, C., Smaragdakis, Y., Xie, T.: DSD-Crasher: A hybrid analysis tool for bug finding. ACM Transactions on Software Engineering and Methodologies (TOSEM) 17(2) (April 2008)

    Google Scholar 

  5. Csallner, C., Tillmann, N., Smaragdakis, Y.: DySy: Dynamic symbolic execution for invariant inference. In: International Conference on Software Engineering (ICSE) (May 2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer and Information Science, University of Oregon, Eugene, OR 97403-1202, USA

    Yannis Smaragdakis

Authors
  1. Yannis Smaragdakis
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Klaus Havelund Rupak Majumdar Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Smaragdakis, Y. (2008). Combining Static and Dynamic Reasoning for the Discovery of Program Properties. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-85114-1_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-85113-4

  • Online ISBN: 978-3-540-85114-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation