软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2010年
11期
2711-2724
,共14页
静态分析%抽象解释%多面体抽象域%凸闭包%强接合%弱接合
靜態分析%抽象解釋%多麵體抽象域%凸閉包%彊接閤%弱接閤
정태분석%추상해석%다면체추상역%철폐포%강접합%약접합
基于约束的多面体抽象域的处理能力主要受限于其高代价的(强)接合操作,即两多面体的凸闭包计算.针对基于约束的多面体抽象域提出了一系列低代价的弱接合操作,以作为凸闭包计算的可靠替代候选.为了能够在分析效率和精度之间取得合理权衡,还提出了一种启发式策略,以把强、弱接合动态地、有机地结合起来进行程序分析.实验结果表明,弱接合能够极大地提升基于约束的多面体抽象域的效率、可扩展性和鲁棒性.
基于約束的多麵體抽象域的處理能力主要受限于其高代價的(彊)接閤操作,即兩多麵體的凸閉包計算.針對基于約束的多麵體抽象域提齣瞭一繫列低代價的弱接閤操作,以作為凸閉包計算的可靠替代候選.為瞭能夠在分析效率和精度之間取得閤理權衡,還提齣瞭一種啟髮式策略,以把彊、弱接閤動態地、有機地結閤起來進行程序分析.實驗結果錶明,弱接閤能夠極大地提升基于約束的多麵體抽象域的效率、可擴展性和魯棒性.
기우약속적다면체추상역적처리능력주요수한우기고대개적(강)접합조작,즉량다면체적철폐포계산.침대기우약속적다면체추상역제출료일계렬저대개적약접합조작,이작위철폐포계산적가고체대후선.위료능구재분석효솔화정도지간취득합리권형,환제출료일충계발식책략,이파강、약접합동태지、유궤지결합기래진행정서분석.실험결과표명,약접합능구겁대지제승기우약속적다면체추상역적효솔、가확전성화로봉성.
