抽象解释论文

《抽象解释论文》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、基于抽象解释的程序分析及其应用摘要：在计算机普遍应用的现代社会，软件特别是大型实时安全攸关软件的可靠性成为计算机界和整个社会都非常关注的问题。现有的形式化软件验证工具都不得不通过近似来处理复杂问题中的计算，抽象解释作为一种在数学模型间进行可靠近似的理论，为各类自动验证工具中不同的近似方法建立起一个统一的形式化框架。抽象解释理论在程序分析和验证研究领域得到了广泛的关注与应用，其应用范围涵盖了程序静态分析、程序变换、程序调试、程序水印等方面。本文分析了现有程序分析和验证典型形式化方法的不足，描述了基于程序不动点语义的抽象解释理论框架，介绍了Galois连接、Widening算子、Na

2、rrowing算子，指出了基于抽象解释理论的程序验证的主要研究方向。并对其近年来的应用现状进行了较为全面的介绍，最后给出了抽象解释理论中尚存在的一些问题及可能的研究方向。关键字：抽象解释；Galois连接；Widening算子；Narrowing算子；程序验证ProgramverificationtechniquesandapplicationbasedontheabstractinterpretationZhoujie【Abstract】：Inahighlycomputer-dependentsociety，reliabilityofsoftware，especiallyofb

3、igreal-timesafetycriticalones，gainsfarrangingattentionfromcomputercommunityandtherestoftheworld.Existingtoolsforformalprogramverifyinghavetodealwithcomplexcomputationthroughapproximatingtosomeextent.Abstractinterpretationisatheoryforsoundapproximationbetweenmathematicmodels，andconstructsaunif

4、yingformalframeworkfordifferentapproximatemethodsofdifferentprogramverificationtools.Abstractinterpretationisdiscussedandappliedwidelyinseveralprogramanalysisandverificationfields，includingstaticanalysis，programtransform，debugging，programwatermarking，andsoon.Thispaperanalyzestheshortcomingsof

5、theexistingtypicalformalismmethodoftheprogramanalysisandverification，introducesGaloisconnection、Wideningoperator、Narrowingoperator，describesthetheoryframeworkofabstractingprogram’sfixpointsemantics，andthenintroducesitsstateoftheartandfuturechallenges.【keyword】：Abstractinterpretation；Galoiscon

6、nection；Wideningoperator；Narrowingoperator；programverification1引言：随着计算机技术在各行各业应用的日益普及，工作在我们身边的各种计算机系统由于其中的软件系统失效经常表现的不尽人意，呈现出脆弱、难以信任的特征，甚至造成不可挽回的损失，因此研究相关的可信软件关键技术以提高软件系统的可信性已经成为十分迫切的需求。在程序可信性分析和验证的研究过程中中，模型检验、定理证明是能够自动化实现的典型形式化方法。模型检验通过遍历系统所有状态空间,能够对有穷状态系统进行自动验证,并自动构造不满足验证性质的反例。对于无穷状态系统或状态数目

7、超出现有计算机处理能力的非常复杂的有穷状态系统,模型检验方法难以解决状态空间爆炸问题。定理证明方法能够应用于解决无穷状态系统的验证问题,但是模型检验是一种自动验证有穷状态系统的技术，其基本思想是通过遍历系统模型的状态空间老检验系统模型是否满足给定的性质。模型检验面临状态空间爆炸的难题，定理证明方法也受到一阶逻辑半可判定性的限制，因为一阶逻辑是半可判定的，理论分析结果表明,机械化的定理证明过程并不能保证停机。计算机科学理论和大规模软、硬件系统的发展需要一种能够处理计算机科学中不可判