چكيده به لاتين
The development of large software systems is a complex and fault-prone process. Faults may occur at any stage of software development. If these faults are not identified and eliminated in time, they can cause a lot of damage in terms of time and money. Nearly three decades of experience have proven that software testing is an effective way to ensure software quality by detecting faults. One of the most important tasks when testing software is to generate appropriate test data. Many methods have been developed to lead the process of generating test data, among which we can mention the concolic testing. Theoretically, the concolic testing can provide high path coverage with the help of a strong constraint solver. But there is no such constraint solver. Existing constraint solvers have shortcomings. One of these shortcomings is the variety of data types supported by these constraint solvers. Most constraint solvers do not support path constraints involving variables with complex data types such as strings, arrays, and structs. And they are not able to solve path constraints involving the black-box function calls, functions whose code is not available. Another issue is that all existing constraint solvers generate a value for each variable present in the path constraint and do not have adequate domain coverage, which leaves many latent faults of the program undetected. In this thesis, to eliminate the shortcomings of existing constraint solvers, an attempt has been made to present a method for producing a constraint solver. In order to evaluate, the proposed constraint solver has been compared and evaluated in terms of supported data types, success in solving path constraints, runtime, and domain coverage with five of the most well-known, newest, and powerful existing constraint solvers, CVC4, S3, Yices2, Z3, and Z3str3. The evaluation results indicate that the proposed constraint solver has been able to greatly improve the mentioned criteria.
