User Tools

Site Tools


Extending CREST with Multiple SMT Solvers and Real Arithmetic (BibTeX)

@inproceedings{DoTruongNguyen-KSE-2010,
  author      = {Quoc Huy Do and Anh Hoang Truong and Ngoc Binh Nguyen},
  booktitle   = {{2010 Second International Conference on Knowledge and Systems Engineering}},
  title       = {{Extending CREST with Multiple SMT Solvers and Real Arithmetic}},
  year        = 2010,
  pages       = {183-187},
  abstract    = {Generating the test inputs, that have high code coverage while minimizing the number of test inputs, is a practical but difficult problem. The application of symbolic execution in combination with SMT solvers gives a promising way to solve it. Recently, there have been several tools that help generating the test inputs for C programs, but their abilities are still limited, depending on the particular chosen SMT solver and most of them currently do not support real arithmetic. We propose an approach to overcome the limitation of unique solver's ability by using multiple SMT solvers and combining their results to get the best solution. We also propose a method of reasoning real arithmetic for symbolic testing. We have implemented this approach in an open source symbolic testing tool called real CREST. Our experimental results are very positive.},
}