HOME JOURNALS CONTACT

Information Technology Journal

Year: 2010 | Volume: 9 | Issue: 2 | Page No.: 349-353
DOI: 10.3923/itj.2010.349.353
Finding Loop Invariants Based on Wu's Characteristic Set Method
Yong Cao and Qing-Xin Zhu

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.

Fulltext PDF Fulltext HTML

How to cite this article
Yong Cao and Qing-Xin Zhu, 2010. Finding Loop Invariants Based on Wu's Characteristic Set Method. Information Technology Journal, 9: 349-353.

Related Articles:
© Science Alert. All Rights Reserved