The Design And Implementation Of Program Verification Tools Base On Invariants

With the rapid development of computer science, software plays an increasingly important role in people's daily life, so the correctness verification of software program got a great deal attention in academic domain. Termination and safety verification are two important parts of program correctness verification, based on Mathematica and generation of invariant, we design and implement a tool for termination and safety verification. The main contributions are summarized as follows:1. The implementation of automatic program invariants generation. Based on Mathematica, we have designed and implemented a tool for automatic program invariant generation, which constructs the linear invariants using CILinear and constructs the polynomial loop invaraints using Aligator. The constructed invariants describe the relationships among the loop program variables, and provide the computation basis for the program correctness verification.2. The implementation of termination verification. First we instrument a counter into program loop to record loop times. Then constructed invariant sets as constraint system and whether counter have minimum as objective function, we transform the termination verification problem into an optimization problem, based on the optimization problem-solving function Minimize in Mathematica, we can not only effectively complete the termination verification, but also generate the exact complexity bound of program loops.3. The implementation of safety verification. First we instrument the assume and statements, establish the propositions for safety verification, construct the verification conditions with the set of invariants, transform the verification of safety into the verification of the validity of the logic formula that the invariants imply the the propositions characterizing safety. Then based on the theorem prover PCS in Theorema, the logical formula can be constructed from a set of invariants implying a formula which specifies the safety property. We can effectively implement the safety verification of program.