Abstract
State-of-the-art solvers for constrained Horn clauses (CHC) are successfully used to generate reachability facts from symbolic encodings of programs. In this paper, we present a new application to test-case generation: if a block of code is provably unreachable, no test case can be generated allowing to explore other blocks of code. Our new approach uses CHC to incrementally construct different program unrollings and extract test cases from models of satisfiable formulas. At the same time, a CHC solver keeps track of CHCs that represent unreachable blocks of code which makes the unrolling process more efficient. In practice, this lets our approach to terminate early while guaranteeing maximal coverage. Our implementation called Horntinuum exhibits promising performance: it generates high coverage in the majority of cases and spends less time on average than state-of-the-art.
Chapter PDF
Similar content being viewed by others
References
Alshmrany, K.M., Aldughaim, M., Bhayat, A., Cordeiro, L.C.: FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs. In: TAP. Lecture Notes in Computer Science, vol. 12740, pp. 85–105. Springer (2021)
Alur, R., BodÃk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-Guided Synthesis. In: FMCAD. pp. 1–17. IEEE (2013)
Anand, S., Godefroid, P., Tillmann, N.: Demand-driven compositional symbolic execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. Lecture Notes in Computer Science, vol. 4963, pp. 367–381. Springer (2008)
Beyer, D., Lemberger, T.: Testcov: Robust test-suite execution and coverage measurement. In: ASE. pp. 1074–1077. IEEE (2019)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: TACAS. LNCS, vol. 1579, pp. 193–207. Springer (1999)
Blicha, M., Fedyukovich, G., Hyvärinen, A.E.J., Sharygina, N.: Transition Power Abstractions for Deep Counterexample Detection. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg (2022)
Böhme, M., Pham, V., Roychoudhury, A.: Coverage-based greybox fuzzing as markov chain. IEEE Trans. Software Eng. 45(5), 489–506 (2019)
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)
Chowdhury, A.B., Medicherla, R.K., Venkatesh, R.: Verifuzz: Program aware fuzzing - (competition contribution). In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS, Part III. Lecture Notes in Computer Science, vol. 11429, pp. 244–249. Springer (2019)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS. LNCS, vol. 2988, pp. 168–176. Springer (2004)
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)
Fedyukovich, G., BodÃk, R.: Accelerating Syntax-Guided Invariant Synthesis. In: TACAS, Part I. LNCS, vol. 10805, pp. 251–269. Springer (2018)
Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Property directed equivalence via abstract simulation. In: CAV. LNCS, vol. 9780, Part II, pp. 433–453. Springer (2016)
Fedyukovich, G., Kaufman, S., BodÃk, R.: Sampling Invariants from Frequency Distributions. In: FMCAD. pp. 100–107. IEEE (2017)
Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving Constrained Horn Clauses Using Syntax and Data. In: FMCAD. pp. 170–178. IEEE (2018)
Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified Invariants via Syntax-Guided Synthesis. In: CAV, Part I. LNCS, vol. 11561, pp. 259–277. Springer (2019)
Fedyukovich, G., Rümmer, P.: Competition report: CHC-COMP-21. In: Hojjat, H., Kafle, B. (eds.) HCVS@ETAPS. EPTCS, vol. 344, pp. 91–108 (2021)
Flanagan, C., Leino, K.R.M.: Houdini: an Annotation Assistant for ESC/Java. In: FME. LNCS, vol. 2021, pp. 500–517. Springer (2001)
Gadelha, M.Y.R., Monteiro, F.R., Cordeiro, L.C., Nicole, D.A.: ESBMC v6.0: Verifying C programs using k-induction and invariant inference - (competition contribution). In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS:, Part III. LNCS, vol. 11429, pp. 209–213. Springer (2019)
Godefroid, P., Kiezun, A., Levin, M.Y.: Grammar-based whitebox fuzzing. In: Gupta, R., Amarasinghe, S.P. (eds.) PLDI. pp. 206–215. ACM (2008)
Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn Verification Framework. In: CAV. LNCS, vol. 9206, pp. 343–361. Springer (2015)
Jaffar, J., Murali, V., Navas, J.A.: Boosting concolic testing via interpolation. In: Meyer, B., Baresi, L., Mezini, M. (eds.) ESEC/FSE. pp. 48–58. ACM (2013)
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-Based Model Checking for Recursive Programs. In: CAV. LNCS, vol. 8559, pp. 17–34 (2014)
Le, H.M.: Llvm-based hybrid fuzzing with libkluzzer (competition contribution). In: Wehrheim, H., Cabot, J. (eds.) FASE. LNCS, vol. 12076, pp. 535–539. Springer (2020)
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)
de Moura, L.M., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS. LNCS, vol. 4963, pp. 337–340. Springer (2008)
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)
Serebryany, K.: Continuous fuzzing with libfuzzer and addresssanitizer. In: SecDev. p. 157. IEEE Computer Society (2016)
Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: ESOP. LNCS, vol. 7792, pp. 574–592. Springer (2013)
Vikram, V., Padhye, R., Sen, K.: Growing A test corpus with bonsai fuzzing. In: ICSE. pp. 723–735. IEEE (2021)
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)
Wüstholz, V., Christakis, M.: Targeted greybox fuzzing with static lookahead analysis. In: Rothermel, G., Bae, D. (eds.) ICSE. pp. 789–800. ACM (2020)
Zalewski, M.: American Fuzzy Lop, https://lcamtuf.coredump.cx/afl/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Zlatkin, I., Fedyukovich, G. (2022). Maximizing Branch Coverage with Constrained Horn Clauses. In: Fisman, D., Rosu, G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. Lecture Notes in Computer Science, vol 13244. Springer, Cham. https://doi.org/10.1007/978-3-030-99527-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-99527-0_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99526-3
Online ISBN: 978-3-030-99527-0
eBook Packages: Computer ScienceComputer Science (R0)