Verifying provisions for post-transaction user input error correction through static program analysis

Software testing is a time-consuming and error-prone process. Automated software verification is an important key to improve software testing. This paper presents a novel approach for the automated approximate verification of provisions of transactions for correcting effects that result from executing database transactions with wrong user inputs. The provision is essential in any database application. The approach verifies the provision through analyzing the source codes of transactions in a database application. It is based on some patterns that in all likelihood exist between the control flow graph of a transaction and the control flow graphs of transactions for correcting some post-transaction user input errors of the former transaction. We have validated the patterns statistically.