KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. Symbolic execution tool, KLEE, capable of automatically generating tests that achieve high coverage on a diverse set of complex and environmentally-intensive programs. We used KLEE to thoroughly check all 89 stand-alone programs in the GNU COREUTILS utility suite, which form the core user-level environment installed on millions of Unix systems, and arguably are the single most heavily tested set of open-source programs in existence. KLEE-generated tests achieve high line coverage — on average over 90% per tool (median: over 94%) — and significantly beat the coverage of the developers’ own hand-written test suites. When we did the same for 75 equivalent tools in the BUSYBOX embedded system suite, results were even better, including 100% coverage on 31 of them. We also used KLEE as a bug finding tool, applying it to 452 applications (over 430K total lines of code), where it found 56 serious bugs, including three in COREUTILS that had been missed for over 15 years. Finally, we used KLEE to cross-check purportedly identical BUSY-BOX and COREUTILS utilities, finding functional correctness errors and a myriad of inconsistencies.

References in zbMATH (referenced in 40 articles )

Showing results 1 to 20 of 40.
Sorted by year (citations)

1 2 next

  1. Bayless, Sam; Kodirov, Nodir; Iqbal, Syed M.; Beschastnikh, Ivan; Hoos, Holger H.; Hu, Alan J.: Scalable constraint-based virtual data center allocation (2020)
  2. Garzella, Jack J.; Baranowski, Marek; He, Shaobo; Rakamarić, Zvonimir: Leveraging compiler intermediate representation for multi- and cross-language verification (2020)
  3. Ish-Shalom, Oren; Itzhaky, Shachar; Manevich, Roman; Rinetzky, Noam: Harnessing static analysis to help learn pseudo-inverses of string manipulating procedures for automatic test generation (2020)
  4. Amadini, Roberto; Andrlon, Mak; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.: Constraint programming for dynamic symbolic execution of JavaScript (2019)
  5. Wang, Wenxi; Søndergaard, Harald; Stuckey, Peter J.: Wombit: a portfolio bit-vector solver using word-level propagation (2019)
  6. Chungha Sung, Brandon Paulsen, Chao Wang: CANAL: A Cache Timing Analysis Framework via LLVM Transformation (2018) arXiv
  7. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  8. Gupta, Shubhani; Saxena, Aseem; Mahajan, Anmol; Bansal, Sorav: Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition (2018)
  9. Lauko, Henrich; Ročkai, Petr; Barnat, Jiří: Symbolic computation via program transformation (2018)
  10. Hutter, Frank; Lindauer, Marius; Balint, Adrian; Bayless, Sam; Hoos, Holger; Leyton-Brown, Kevin: The configurable SAT solver challenge (CSSC) (2017)
  11. Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution (2017)
  12. Lampropoulos, Leonidas; Gallois-Wong, Diane; Hriţcu, Cătălin; Hughes, John; Pierce, Benjamin C.; Xia, Li-yao: Beginner’s Luck: a language for property-based generators (2017)
  13. Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei: A generic framework for symbolic execution: a coinductive approach (2017)
  14. Rocha, Camilo; Meseguer, José; Muñoz, César: Rewriting modulo SMT and open system analysis (2017)
  15. Rusu, Vlad; Arusoaie, Andrei: Executing and verifying higher-order functional-imperative programs in Maude (2017)
  16. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  17. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  18. Zheng, Yunhui; Ganesh, Vijay; Subramanian, Sanu; Tripp, Omer; Berzish, Murphy; Dolby, Julian; Zhang, Xiangyu: Z3str2: an efficient solver for strings, regular expressions, and length constraints (2017)
  19. Cai, Jun; Zou, Peng; Ma, Jinxin; He, Jun: SwordDTA: A dynamic taint analysis tool for software vulnerability detection (2016) ioport
  20. Saarikivi, Olli; Heljanko, Keijo: LCTD: test-guided proofs for C programs on LLVM (2016)

1 2 next