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 [email protected].

1. Oasis: Concolic Execution Driven by Test Suites and Code Modifications
   Olivier Crameri, Rekha Bachwani, Tim Brecht, Ricardo Bianchini, Dejan Kostic, Willy Zwaenepoel
   École Polytechnique Fédérale de Lausanne (EPFL), Technical report LABOS-REPORT-2009-002, 2009

2. 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

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

4. 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

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

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

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

8. 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

9. 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

10. 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

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

12. 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

13. 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

14. 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

15. 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

16. 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

17. 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

18. 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

19. 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

20. 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

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

22. 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

23. 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

24. 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

25. 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

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

27. 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

28. 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

29. 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

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

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

32. 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

33. 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

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

35. Locating Software Faults Based on Minimum Debugging Frontier Set
    Feng Li, Zhiyuan Li, Wei Huo, Xiaobing Feng
    IEEE Transactions on Software Engineering, August 2017

36. Invasive Software Testing: Mutating Target Programs to Diversify Test Exploration for High Test Coverage
    Yunho Kim, Shin Hong, Bongseok Ko, Duy Loc Phan and Moonzoo Kim
    IEEE International Conference on Software Testing, Validation and Verification (ICST), 2018

37. COMPI: Concolic Testing for MPI Applications
    Hongbo Li, Sihuan Li, Zachary Benavides, Zizhong Chen, Rajiv Gupta
    IEEE International Parallel and Distributed Processing Symposium (IPDPS), 2018.

38. Reducer-Based Construction of Conditional Verifiers
    Dirk Beyer, Marie-Christine Jakobs, Thomas Lemberger, Heike Wehrheim
    ACM/IEEE International Conference on Software Engineering (ICSE), 2018

39. Automatically Generating Search Heuristics for Concolic Testing
    Sooyoung Cha, Seongjoon Hong, Junhee Lee, Hakjoo Oh
    ACM/IEEE International Conference on Software Engineering (ICSE), 2018

40. Template-Guided Concolic Testing via Online Learning
    Sooyoung Cha, Seonho Lee, Hakjoo Oh
    ACM/IEEE International Conference on Automated Software Engineering (ASE), 2018