Abstract:
Loop invariants are important parts in program verification and proof. Correspondingly, techniques for automatically checking and finding invariants have been studied for many years. In present study, an approach using Wu's characteristic set method for automatically finding polynomial invariants of imperative programs is presented. Present method is based on the algebraic theory of polynomial set over polynomial rings, which have wider application domain. We implement this method with the computer algebra tools MMP. The application of the method is demonstrated on a few examples. Compared with other polynomial algebraic approaches, our method is more efficient through experiments.
Subscribe Today 
