计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2010年
9期
76-80
,共5页
程序验证%循环不变式%带量词的布尔公式
程序驗證%循環不變式%帶量詞的佈爾公式
정서험증%순배불변식%대량사적포이공식
构造循环不变式是程序验证的核心问题之一.主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值,然而程序执行过程中变量都是用有限长度的位向量来表示,无限数域上的循环不变式在有限数域的程序中可能不再是不变式,反之亦然.针对这一问题,本文给出一种基于QBF求解的构造有限数域上循环不变式的方法.该方法可用于构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,支持加、减、乘、除、移位、位操作等,允许不变式中出现量词.本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值.
構造循環不變式是程序驗證的覈心問題之一.主流的循環不變式構造方法通常假設程序中的變量在無限數域上取值,然而程序執行過程中變量都是用有限長度的位嚮量來錶示,無限數域上的循環不變式在有限數域的程序中可能不再是不變式,反之亦然.針對這一問題,本文給齣一種基于QBF求解的構造有限數域上循環不變式的方法.該方法可用于構造類型豐富的不變式,包括線性(或多項式)等式(或不等式)不變式,支持加、減、乘、除、移位、位操作等,允許不變式中齣現量詞.本文也例證瞭該方法在程序終止性證明、循環上界分析、程序正確性證明等方麵的應用價值.
구조순배불변식시정서험증적핵심문제지일.주류적순배불변식구조방법통상가설정서중적변량재무한수역상취치,연이정서집행과정중변량도시용유한장도적위향량래표시,무한수역상적순배불변식재유한수역적정서중가능불재시불변식,반지역연.침대저일문제,본문급출일충기우QBF구해적구조유한수역상순배불변식적방법.해방법가용우구조류형봉부적불변식,포괄선성(혹다항식)등식(혹불등식)불변식,지지가、감、승、제、이위、위조작등,윤허불변식중출현량사.본문야예증료해방법재정서종지성증명、순배상계분석、정서정학성증명등방면적응용개치.
