资源描述：
《基于约束的多面体抽象域的弱接合》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.ac.cnJournalofSoftware,Vol.21,No.11,November2010,pp.2711−2724http://www.jos.org.cndoi:10.3724/SP.J.1001.2010.03664Tel/Fax:+86-10-62562563©byInstituteofSoftware,theChineseAcademyofSciences.Allrightsreserved.∗基于约束的多面体抽象域的
2、弱接合+陈立前,王戟,刘万伟(国防科学技术大学计算机学院并行与分布处理国家重点实验室,湖南长沙410073)WeakJoinfortheConstraint-BasedPolyehdraAbstractDomain+CHENLi-Qian,WANGJi,LIUWan-Wei(NationalLaboratoryforParallelandDistributedProcessing,SchoolofComputer,NationalUniversityofDefenseTechnology,Changsha410073
3、,China)+Correspondingauthor:E-mail:wj@nudt.edu.cnChenLQ,WangJ,LiuWW.Weakjoinfortheconstraint-basedpolyehdraabstractdomain.JournalofSoftware,2010,21(11):2711−2724.http://www.jos.org.cn/1000-9825/3664.htmAbstract:Themaintractabilityproblemoftheconstraint-basedpol
4、yhedraabstractdomaincanbederivedfromthecostly(strong)joinoperation,thatis,theconvexhullcomputation.Thispaperpresentsaseriesofcheapweakjoinoperationsasasoundsubstitutionfortheconvexhulloperationoftheconstraint-basedpolyhedradomain.Toachieveatrade-offbetweeneffic
5、iencyandprecision,aheuristicstrategyisproposedwhichdynamicallycombinesbothstrongjoinandweakjoinduringprogramanalysis.Experimentalresultsshowthattheweakjoinoperationcansignificantlyimprovetheefficiency,scalabilityandrobustnessoftheconstraint-basedpolyhedradomain
6、.Keywords:staticanalysis;abstractinterpretation;polyhedraabstractdomain;convexhull;strongjoin;weakjoin摘要:基于约束的多面体抽象域的处理能力主要受限于其高代价的(强)接合操作,即两多面体的凸闭包计算.针对基于约束的多面体抽象域提出了一系列低代价的弱接合操作,以作为凸闭包计算的可靠替代候选.为了能够在分析效率和精度之间取得合理权衡,还提出了一种启发式策略,以把强、弱接合动态地、有机地结合起来进行程序分析.实验结果表明,
7、弱接合能够极大地提升基于约束的多面体抽象域的效率、可扩展性和鲁棒性.关键词:静态分析;抽象解释;多面体抽象域;凸闭包;强接合;弱接合中图法分类号:TP311文献标识码:A[1,2]抽象解释是一种对数学结构进行近似(或抽象)的通用理论.该理论在静态分析中的一个重要应用是数[3]值程序分析,旨在自动产生程序中某程序点处的数值不变式,即每次程序执行均满足的数值变量间的关系(如[4]x−y≤1).基于抽象解释的数值程序分析在编译优化、程序分析与验证等方面都有着广泛的应用,可用来分析程序中是否有除零错、数组越界、整数溢出等运行
8、时错误,也可以用来分析程序中的断言以及契约中的前置条件、后置条件和不变式.抽象域是抽象解释理论中的一个核心概念,由两部分构成:一个计算机可表示的对象(称为域元素)集合以∗SupportedbytheNationalNaturalScienceFoundationofChinaunderGrantNos.60725206,60921062,608
