四川大学学报：工程科学版2012，Vol.44Issue(4)：115-121,7.
用Dixon结式产生非线性循环不变式
Non-linear Loop Invariant Generation Using Dxion Resultant
摘要
Abstract
TO solve the partial correct problem of loop program, an algorithm was presented to generate non-linear loop invariant by computing Dixon resultant based on algebraic transition system and constraint system. The loop program was firstly transformed to an al- gebraic transition system, then a polynomial set was constructed from algebraic transition relation and invariant template, and a con- straint system w. r. t template variable was obtained by computing Dixon resultant. Finally the constraint system was resolved to get in- variant. The algorithm was effective to whether single-path or multi-path programs through case study.关键词
循环不变式/Dixon结式/模板/约束Key words
loop invariant/Dixon resultant/template/constraints分类
计算机与自动化引用本文复制引用
余伟,冯勇..用Dixon结式产生非线性循环不变式[J].四川大学学报：工程科学版,2012,44(4):115-121,7.基金项目
国家“973”计划资助项目 （）
国家自然科学基金面上项目 （）
国家自然科学基金重大研究计划资助项目 （）
