[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Leveraging Program Structure for Test Case Generation

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15055))

  • 1 Accesses

Abstract

We present a novel language-agnostic approach to test case generation from a logic program representation generated by an existing framework. This is nontrivial for two reasons: since in such representation basic statements are usually composed into complex formulas, the trace enumerator cannot distill statements that are yet to be covered, and since the formulas obtained this way are more complex, the satisfiability checks are costlier and their number has to be kept low. Our approach performs an accelerated trace enumeration exploiting the program structure on the go. Our new implementation on top of the Horntinuum test case generator calls an SMT solver incrementally to achieve a significant performance increase. Furthermore, it has found many new test cases in public benchmarks that state-of-the-art did not find.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 139.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.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

Notes

  1. 1.

    This feature is disabled in our implementation to allow us to focus solely on enumeration of traces.

References

  1. Alshmrany, K.M., Aldughaim, M., Bhayat, A., Cordeiro, L.C.: FuSeBMC v4: smart seed generation for hybrid fuzzing. In: FASE 2022. LNCS, vol. 13241, pp. 336–340. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99429-7_19

    Chapter  Google Scholar 

  2. Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 367–381. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_28

    Chapter  MATH  Google Scholar 

  3. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45319-9_19

    Chapter  MATH  Google Scholar 

  4. Beyer, D.: Software testing: 5th comparative evaluation: test-comp 2023. In: Lambers, L., Uchitel, S. (eds.) FASE 2023. LNCS, vol. 13991, pp. 309–323. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30826-0_17

  5. Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25–32. IEEE (2009)

    Google Scholar 

  6. Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16

    Chapter  MATH  Google Scholar 

  7. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    Chapter  MATH  Google Scholar 

  8. Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23534-9_2

    Chapter  MATH  Google Scholar 

  9. Blicha, M., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: TACAS 2022. LNCS, vol. 13243, pp. 524–542. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_29

    Chapter  MATH  Google Scholar 

  10. Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_7

    Chapter  MATH  Google Scholar 

  11. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. In: LICS, pp. 428–439. IEEE (1990)

    Google Scholar 

  12. Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) OSDI, pp. 209–224. USENIX Association (2008)

    Google Scholar 

  13. Chakarov, A., Fedchin, A., Rakamarić, Z., Rungta, N.: Better Counterexamples for Dafny. In: TACAS 2022, Part I. LNCS, vol. 13243, pp. 404–411. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99524-9_23

    Chapter  MATH  Google Scholar 

  14. Chechik, M., Gurfinkel, A.: A framework for counterexample generation and exploration. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 220–236. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31984-9_17

    Chapter  MATH  Google Scholar 

  15. Csallner, C., Smaragdakis, Y.: Check ‘n’ crash: combining static checking and testing. In: Roman, G., Griswold, W.G., Nuseibeh, B. (eds.) ICSE, pp. 422–431. ACM (2005)

    Google Scholar 

  16. Fedyukovich, G., Kaufman, S., Bodík, R.: Sampling invariants from frequency distributions. In: FMCAD, pp. 100–107. IEEE (2017)

    Google Scholar 

  17. Godefroid, P., Kiezun, A., Levin, M.Y.: Grammar-based whitebox fuzzing. In: Gupta, R., Amarasinghe, S.P. (eds.) PLDI, pp. 206–215. ACM (2008)

    Google Scholar 

  18. Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281–292. ACM (2008)

    Google Scholar 

  19. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_20

    Chapter  MATH  Google Scholar 

  20. Heizmann, M., et al.: Ultimate automizer with an on-demand construction of Floyd-Hoare automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part II. LNCS, vol. 10206, pp. 394–398. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_30

    Chapter  MATH  Google Scholar 

  21. Hojjat, H., Rümmer, P.: The ELDARICA horn solver. In: FMCAD, pp. 158–164. IEEE (2018)

    Google Scholar 

  22. Kahsai, T., Rümmer, P., Schäf, M.: JayHorn: a Java model checker. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019, Part I. LNCS, vol. 11429, pp. 214–218. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_16

    Chapter  MATH  Google Scholar 

  23. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  24. Le, H.M.: LLVM-based hybrid fuzzing with LibKluzzer (competition contribution). In: FASE 2020. LNCS, vol. 12076, pp. 535–539. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45234-6_29

    Chapter  MATH  Google Scholar 

  25. Mathis, B., Gopinath, R., Mera, M., Kampmann, A., Höschele, M., Zeller, A.: Parser-directed fuzzing. In: McKinley, K.S., Fisher, K. (eds.) PLDI, pp. 548–560. ACM (2019)

    Google Scholar 

  26. Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for rust programs. In: ESOP 2020. LNCS, vol. 12075, pp. 484–514. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44914-8_18

    Chapter  MATH  Google Scholar 

  27. McMillan, K.L., Rybalchenko, A.: Solving constrained Horn clauses using interpolation. In: Technical report, MSR-TR-2013-6 (2013)

    Google Scholar 

  28. Metta, R., Medicherla, R.K., Karmarkar, H.: VeriFuzz: good seeds for fuzzing (competition contribution). In: FASE 2022. LNCS, vol. 13241, pp. 341–346. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99429-7_20

    Chapter  MATH  Google Scholar 

  29. 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). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  MATH  Google Scholar 

  30. Rothenberg, B.-C., Grumberg, O.: Sound and complete mutation-based program repair. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 593–611. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_36

    Chapter  MATH  Google Scholar 

  31. Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H.C. (eds.) FSE, pp. 263–272. ACM (2005)

    Google Scholar 

  32. Vikram, V., Padhye, R., Sen, K.: Growing a test corpus with bonsai fuzzing. In: ICSE, pp. 723–735. IEEE (2021)

    Google Scholar 

  33. Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with java pathfinder. In: Avrunin, G.S., Rothermel, G. (eds.) ISSTA, pp. 97–107. ACM (2004)

    Google Scholar 

  34. Wüstholz, V., Christakis, M.: Targeted greybox fuzzing with static lookahead analysis. In: Rothermel, G., Bae, D. (eds.) ICSE, pp. 789–800. ACM (2020)

    Google Scholar 

  35. Zlatkin, I., Fedyukovich, G.: Maximizing branch coverage with constrained horn clauses. In: Fisman, D., Rosu, G. (eds.) TACAS, Part II. LNCS, vol. 13244, pp. 254–272. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99527-0_14

    Chapter  Google Scholar 

Download references

Acknowledgments

The work is supported by the National Science Foundation grant 2106949 and by a gift from the Ethereum Foundation.

Author information

Authors and Affiliations

  1. Florida State University, Tallahassee, FL, USA

    Ilia Zlatkin & Grigory Fedyukovich

Authors
  1. Ilia Zlatkin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Grigory Fedyukovich
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Grigory Fedyukovich .

Editor information

Editors and Affiliations

  1. Indian Institute of Technology Bombay, Mumbai, Maharashtra, India

    S. Akshay

  2. Stanford University, Stanford, CA, USA

    Aina Niemetz

  3. University of Colorado, Boulder, CO, USA

    Sriram Sankaranarayanan

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zlatkin, I., Fedyukovich, G. (2025). Leveraging Program Structure for Test Case Generation. In: Akshay, S., Niemetz, A., Sankaranarayanan, S. (eds) Automated Technology for Verification and Analysis. ATVA 2024. Lecture Notes in Computer Science, vol 15055. Springer, Cham. https://doi.org/10.1007/978-3-031-78750-8_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-78750-8_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-78749-2

  • Online ISBN: 978-3-031-78750-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation