摘要
Loop invariants play a major role in software verification. In this paper, based on finite difference techniques, a formal characterization for equality loop invariants is presented. Integrating the formal characterization with the automatic verification approach in [5], the algorithm for automatic proving or disproving equality loop invariants is presented. The effectiveness of the algorithm is demonstrated with the experimental results.
- 出版日期2015-4
- 单位中国人民解放军国防科学技术大学