CAUT(C Analysis and Unit Testing)

Software testing is the most commonly adopted technique to ensure software quality. A program is usually composed of units, where a unit contains a number of functions. Unit testing is aimed to independently check functional correctness of a unit.

CAUT is a DSE (dynamic symbolic execution)-based tool to automatically generate test data for C program at unit/program testing level.
It builds on CIL and uses lp_solve and Z3 as the underlying constrait solvers. It supports constraint reasoning on both scalar types and derived types, i.e., structures, arrays and pointers (equality/inequality constraints). It currently supports the coverage-driven testing on branch and MC/DC criteria. And it's easy to be extended to support other logical coverage criteria, like condition, condition/decision or multiple coverage. Up to now, serveral path exploration strategies have been implemented on CAUT. CAUT is only tested on Linux-Ubuntu 32 bit. You can download from our github (updated on 04/01/2014) and a simple video demo is here.


--------
update 2013.5: we have implemented some coverage-based white-box testing techniques on C program at unit testing level.

update 2014.3: our paper on coverage-driven testing has been accepted on SERE 2014! (see References for details)

update 2014.4: we have extended CAUT from the unit testing level to the whole program testing level.

update 2014.9: we have implemented a data flow testing (in particular for all def-use coverage criterion) framework on top of our DSE engine, which combines with the counter-example guided abstract refinement (CEGAR)-based model checking technique to futher improve the testing performance. This combined data flow testing approach combines the strengths of both techniques.

update 2014.12: our paper on "Combining Symbolic Execution and Model Checking for Data Flow Testing" was accepted by ICSE 2015! (see References for details)

update 2015.4: we conduct a detailed survey on data flow testing, and the technical report is ready! (see References for details)

future update: we will make our tool open source soon!

Input/Output

CAUT takes a C unit/program under test and a target coverage criterion (statement, branch, MC/DC, all def-use coverage) as input, and output coverage-driven test data. If you want to know more details, you can refer to some papers at reference part.

Bug Report

If you find any bugs in CAUT or any questions about CAUT, please do not hesitate to contact me. Let's make it better!

Email: tsuletgo@gmail.com

Ting Su, here is my CV (updated on 12/2014), my LinkedIn and my Homepage.

I am a Ph.D student from East China Normal University and surpervised by the following outstanding professors: GeguangPu, Jifeng He.

I currently move to UC Davis as a visiting Ph.D student in Prof. Zhendong Su's group.

Department: Software Engineering Institute, East China Normal University

Address: NO.3663, North Zhongshan Road, Shanghai, China

References

[1]. Ting Su, Ke Wu, Weikai Miao, Geguang Pu, Jifeng He, Yuting Chen, Zhendong Su. A Survey on Data Flow Testing. Technical Report 2015. pdf

[2]. Ting Su, Zhoulai Fu, Geguang Pu, Jifeng He, Zhendong Su. Combining Symbolic Execution and Model Checking for Data Flow Testing. ICSE 2015 (18.5%). pdf

Data flow testing (DFT) focuses on the flow of data through a program. Desipte its higher fault-detection ability over other structural testing techniques, practical DFT remains a significant challenge. This paper tackles this challenge by introducing a hybrid DFT framework: (1) The core of our framework is based on Dynamic Symbolic Execution (DSE), enhanced with a novel guided path search strategy to improve testing performance; and (2) we systematically cast the DFT problem as reachability checking in software model checking to complement our DSE-based approach, yielding a practical hybrid DFT technique that combines the two approaches's respective strengths. Evaluated on both open source and industrial programs, our DSE-based approach improves DFT performance by 60~80% in terms of testing time compared with state-of-the-art search strategies, while our combined technique further reduces 40% testing time and improves data-flow coverage by 20% by eliminating infeasile test objectives. This combined approach also enables the cross-checking of each component for reliable and robust testing results.

[3]. Ting Su, Siyuan Jiang, Geguang Pu, Bin Fang, Jifeng He, Jun Yan, Jianjun Zhao. Automated Coverage-Driven Test Data Generation Using Dynamic Symbolic Execution. SERE 2014 (30%). pdf

Recently code transformations or tailored fitness functions are adopted to achieve coverage (structural or logical criterion) driven testing to ensure software reliability. However, some internal threats like negative impacts on underlying search strategies or local maximum exist. So we propose a dynamic symbolic execution (DSE) based framework combined with a path filtering algorithm and a new heuristic path search strategy, i.e., predictive path search, to achieve faster coverage-driven testing with lower testing cost. The empirical experiments (three open source projects and two industrial projects) show that our approach is effective and efficient. For the open source projects w.r.t branch coverage, our approach in average reduces 25.5% generated test cases and 36.3% solved constraints than the traditional DSE-based approach without path filtering. And the presented heuristic strategy, on the same testing budget, improves the branch coverage by 26.4% and 35.4% than some novel search strategies adopted in KLEE and CREST.

[4]. Xiao Yu, Shuai Sun, Geguang Pu, Siyuan Jiang and Zheng Wang, A Parallel Approach to Concolic Testing with Low-cost Synchronization, ENTCS 2011. pdf

[5]. Tao Sun, Zheng Wang, Geguang Pu, Xiao Yu, Zongyan Qiu and Bin Gu, Towards Scalable Compositional Test Generation, QSIC 2009. pdf

[6]. Zheng Wang, Xiao Yu, Tao Sun, Geguang Pu, Zuohua Ding and Jueliang Hu, Test Data Generation for Derived Types in C Program, TASE 2009. pdf


Thanks

I appreciate the following smart people who have made great contributions to this project:

Geguang Pu, Zheng Wang, Siyuan Jiang, Xiao Yu, Zhaotan Fang, Bo Li, Sihang Shao, Mengdi Wang, Jingyi Yang, Jiazheng Yu.