CAJ | 학술논문

程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质.基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要.本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式.在此基础上,本文还对数组等复杂语法结构进行了建模和抽象.实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题.
정서적정학성험증일직이래도시계산궤과학중적일개도전성문제,추상해석이론위정서정태분석제공료일개통용광가,가이재편역시자동지추도정서적동태성질.기우추상해석적수치정서분석가이자동추도정서중수치변량간적불변식관계,저대우편역우화、정서착오검사지관중요.본문건립병실현료일개면향C화Fortran정서병지지과정간분석적수치정서분석광가화공구,C혹Fortran원정서경과예처리후전화위구유통일격식적중간표시형식,연후기우해중간표시추취여원정서어의등개적어의등식,최후재해어의등식상진행불동점질대계산종이득도정서불변식.재차기출상,본문환대수조등복잡어법결구진행료건모화추상.실험결과표명,해공구구유교고적가확전성、정도,병능구처리대부분인수조적사용이대래적정서분석상적문제.