A Program Verification And Testing Tool Based On Symbolic Execution And Constraint Solving

With the rapid development of software technology, programs are becoming larger and more complex. During software development process, most programmers analyze and test programs manually. This work is time consuming and cannot ensure good quality of software product. If there is a tool that can analyze programs and generate test cases automatically, the reliability of software will be improved dramatically and considerable resources will be saved. For that purpose many tools have been developed. However, few of them can really generate test cases "automatically". Moreover, the variable types they can handle are quite limited and most of them can only be applied in unit testing.For this reason, the thesis presents an approach based on Constraint Satisfaction, Symbolic Execution and Extended Finite State Machines. It can analyze programs written in a subset of the C programming language. This approach can verify program correctness approximately, or generate a set of test cases according to some coverage criterion in software testing. We also developed an automaitc tool which can analyze complex programs containing several functions. It can deal with data types such as integer, real and their arrays. Compared with other similar tools, it's highly automatic.At the end of this thesis, we also discuss the automatic test case generation for database application programs, and describe a supporting tool. This tool can handle a subset of SQL automatically. It can take account of an assertion to be satisfied in the testing, and generate a set of constraints for further solution. The necessary test data can be extracted from the solution.