CREST

Concolic test generation tool for C

View project on GitHub

CREST is an automatic test generation tool for C.

CREST works by inserting instrumentation code (using CIL) into a target program to perform symbolic execution concurrently with the concrete execution. The generated symbolic constraints are solved (using Yices) to generate input that drive the test execution down new, unexplored program paths.

CREST currently only reasons symbolically about linear, integer arithmetic. CREST should be usable on any modern Linux or Mac OS X system. For further building and usage information, see the README file. You may also want to check out the FAQ.

Further questions? Please e-mail the CREST-users mailing list (CREST-users at googlegroups.com, searchable at https://groups.google.com/forum/#!forum/crest-users).

A short paper and technical report about the search strategies in CREST are available at the homepage of Jacob Burnim.

News: CREST 0.1.2 is now available. It can be downloaded at https://github.com/jburnim/crest/releases/tag/v0.1.2. This is a bug fix release – several build issues are fixed, as well as a bug in instrumenting unary expressions.

News: Heechul Yun has extended CREST to support non-linear arithmetic (using Z3). For more information, see: https://github.com/heechul/crest-z3 and https://github.com/heechul/crest-z3/blob/master/README-z3.

Publications

Many research groups have built on top of CREST. If you would like your paper added to the list below, please contact jburnim@gmail.com.

  1. Analysis and Detection of SQL Injection Vulnerabilities via Automatic Test Case Generation of Programs
    M Ruse, T Sarkar, S Basu
    IEEE/IPSJ International Symposium on Applications and the Internet (SAINT), 2010

  2. ParSym: Parallel Symbolic Execution
    Junaid Haroon Siddiqui, Sarfraz Khurshid
    IEEE International Conference on Software Technology and Engineering (ICSTE), 2010

  3. Directed Test Suite Augmentation: Techniques and Tradeoffs
    Zhihong Xu, Yunho Kim, Moonzoo Kim, Gregg Rothermel, Myra Cohen
    ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2010

  4. Striking a New Balance Between Program Instrumentation and Debugging Time
    Olivier Crameri, Ricardo Bianchini, Willy Zwaenepoel
    ACM EuroSys Conference on Computer Systems (EuroSys), 2011

  5. Toward Online Testing of Federated and Heterogeneous Distributed Systems
    Marco Canini, Vojin Jovanovic, Daniele Venzano, Boris Spasojevic, Olivier Crameri, and Dejan Kostic
    USENIX Annual Technical Conference (ATC), 2011

  6. Online testing of federated and heterogeneous distributed systems
    Marco Canini, Vojin Jovanović, Daniele Venzano, Dejan Novaković, Dejan Kostić
    ACM SIGCOMM Conference, 2011

  7. SCORE: a Scalable Concolic Testing Tool for Reliable Embedded Software
    Yunho Kim, Moonzoo Kim
    Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2011

  8. MAGIC: Path-Guided Concolic Testing
    Zhanqi Cui, Wei Le, Mary Lou Soffa, Linzhang Wang, Xuandong Li
    University of Virginia Dept. of Computer Science Tech Report, 2011

  9. Extracting and verifying cryptographic models from C protocol code by symbolic execution
    Aizatulin, Gordon, Jürjens
    ACM SIGSAC Conference on Computer and Communications Security (CCS), 2011

  10. Enhancing structural software coverage by incrementally computing branch executability
    Mauro Baluda, Pietro Braione, Giovanni Denaro, Mauro Pezzè
    Software Quality Journal, December 2011

  11. A Scalable Distributed Concolic Testing Approach: An Empirical Evaluation
    Moonzoo Kim, Yunho Kim, Gregg Rothermel
    IEEE International Conference on Software Testing, Verification and Validation (ICST), 2012

  12. Industrial Application of Concolic Testing on Embedded Software: Case Studies
    Moonzoo Kim, Yunho Kim, Yoonkyu Jang
    IEEE International Conference on Software Testing, Verification and Validation (ICST), 2012

  13. Industrial Application of Concolic Testing Approach: A Case Study on libexif by Using CREST-BV and KLEE
    Y Kim, M Kim, YJ Kim, Y Jang
    ACM/IEEE International Conference on Software Engineering (ICSE), 2012

  14. Dynamic Symbolic Execution Guided by Data Dependency Analysis for High Structural Coverage
    TheAnh Do, A.C.M. Fong, Russel Pears, International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), 2012

  15. Using Concolic Testing to Refine Vulnerability Profiles in FUZZBUSTER
    David J. Musliner, Jeffrey M. Rye, Tom Marble
    IEEE International Conference on Self-Adaptive and Self-Organizing Systems (SASO), 2012

  16. FoREnSiC - An Automatic Debugging Environment for C Programs
    Roderick Bloem, Rolf Drechsler, Goerschwin Fey, Alexander Finder, Georg Hofferek, Robert Koenighofer, Jaan Raik, Urmas Repinski, Andre Suelflow
    International Haifa Verification Conference (HVC), 2012

  17. Feedback-Directed Unit Test Generation for C/C++ using Concolic Execution
    Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta
    ACM/IEEE International Conference on Software Engineering (ICSE), 2013

  18. Con2colic Testing
    Azadeh Farzan, Andreas Holzer, Niloofar Razavi, Helmut Veith
    Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 2013

  19. Meta-control for Adaptive Cybersecurity in FUZZBUSTER
    David J. Musliner, Scott E. Friedman, Jeffrey M. Rye
    IEEE International Conference on Self-Adaptive and Self-Organizing Systems (SASO), 2013

  20. CCCD: Concolic Code Clone Detection
    Daniel E. Krutz, Emad Shihab
    IEEE Working Conference on Reverse Engineering (WCRE), 2013

  21. Improving Automated Cybersecurity by Generalizing Faults and Quantifying Patch Performance
    Scott E. Friedman, David J. Musliner, Jeffrey Rye
    International Journal on Advances in Security, 2014

  22. Software testing with code-based test generators: data and lessons learned from a case study with an industrial software component
    Pietro Braione, Giovanni Denaro, Andrea Mattavelli, Mattia Vivanti, Ali Muhammad
    Software Quality Journal, 2014

  23. How We Get There: A Context-Guided Search Strategy in Concolic Testing
    Hyunmin Seo, Sunghun Kim
    ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2014

  24. SMCDCT: A Framework for Automated MC/DC Test Case Generation Using Distributed Concolic Testing Sangharatna Godboley, Subhrakanta Panda, Durga Prasad Mohapatra International Conference on Distributed Computing and Internet Technology (ICDCIT), 2015

  25. PBCOV: a property-based coverage criterion
    Kassem Fawaz, Fadi Zaraket, Wes Masri, Hamza Harkous
    Software Quality Journal, March 2015

  26. Directed test suite augmentation: an empirical investigation
    Zhihong Xu, Yunho Kim, Moonzoo Kim, Myra B. Cohen, Gregg Rothermel
    Software Testing, Verification and Reliability, March 2015

  27. Systematic Testing of Reactive Software with Non-deterministic Events: A Case Study on LG Electric Oven
    Yongbae Park, Shin Hong, Moonzoo Kim, Dongju Lee, Junhee Cho
    ACM/IEEE International Conference on Software Engineering (ICSE), 2015

  28. Reusing constraint proofs in program analysis
    Andrea Aquino, Francesco A. Bianchi, Meixian Chen, Giovanni Denaro, Mauro Pezzè
    ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), 2015

  29. Abstraction-driven Concolic Testing
    Przemysław Daca, Ashutosh Gupta, Thomas A. Henzinger International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016

  30. CLORIFI: software vulnerability discovery using code clone verification
    Hongzhe Li, Hyuckmin Kwon, Jonghoon Kwon, Heejo Lee
    Concurrency and Computation: Practice and Experience, April 2016

  31. PAC learning-based verification and model synthesis
    Yu-Fang Chen, Chiao Hsieh, Ondřej Lengál, Tsung-Ju Lii, Ming-Hsien Tsai, Bow-Yaw Wang, Bow-Yaw Wang
    ACM/IEEE International Conference on Software Engineering (ICSE), 2016

  32. Design of a Modified Concolic Testing Algorithm with Smaller Constraints
    Yavuz Koroglu, Alper Sen
    International Workshop on Constraints in Software Testing, Verification and Analysis (CSTVA), 2016

  33. An improved distributed concolic testing approach Sangharatna Godboley, Durga Prasad Mohapatra, Avijit Das, Rajib Mall Software: Practice and Experience, February 2017