微信服务号

微信订阅号

2025年3月24日 17:27 星期一
首页 > 过刊浏览>2008年第19卷第1期 >17-26
PDF HTML阅读 XML下载 导出引用 引用提醒
基于抽象解释理论的程序验证技术
作者:
基金项目:

Supported by the National Natural Science Foundation of China under Grant Nos.60473057, 90604007 (国家自然科学基金)


Program Verification Techniques Based on the Abstract Interpretation Theory
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [46]
    • |
  • 相似文献
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.

    Abstract:

    The abstract interpretation theory was proposed by P. Cousot and R. Cousot in 1977, and is widely used in the program’s static analysis domain to construct and approximate the program’s fixpoint semantics. This paper describes the abstract interpretation framework of the program semantics based on the Galois connection, and then discusses three typical applications of the abstract interpretation theory: The program transformation, the program verification techniques about the safety property and the program verification techniques about the liveness property. Finally, it points out the main directions of the program verification techniques based on the abstract interpretation theory.

    参考文献
    [1] Cousot P, Cousot R. Abstract interpretation: A unified Lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of the 4th POPL. Los Angeles: ACM Press, 1977. 238-252. http://www.di.ens.fr/～cousot/ COUSOTpapers/POPL77.shtml
    [2] Cousot P, Cousot R. Systematic design of program analysis frameworks. In: Proc. of the 6th POPL. San Antonio: ACM Press, 1979. 69-282. http://www.di.ens.fr/～cousot/COUSOTpapers/POPL79.shtml
    [3] Cousot P, Cousot R. Abstract interpretation frameworks. Journal of Logic and Computer, 1992,2(4):511-547.
    [4] Cousot P, Cousot R. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe M, Wirsing M, eds. Proc. of the PLILP’92. LNCS 631, Springer-Verlag, 1992. 269-295.
    [5] Cousot P. Abstract interpretation based formal methods and future chanllenges. In: Wilhelm R, ed. Informatics——10 Years Back, 10 Years Ahead. Berlin, Heidelberg: Springer-Verlag, 2000. 138-156.
    [6] Cousot P, Cousot R. Abstract interpretation based program testing. In: Proc. of the SSGRR 2000 Computer & eBusiness Int’l Conf. 2000. Compact disk paper 248. http://www.di.ens.fr/～cousot/COUSOTpapers/SSGRRP-00-PC-RC.shtml
    [7] Cousot P, Cousot R. Basic concepts of abstract interpretation. In: René J, ed. Building the Information Society. Toulouse: Kluwer Academic Publishers, 2004. 359-366.
    [8] Cousot P, Cousot R. Refining model checking by abstract interpretation. Automated Software Engineering Journal (Special Issue on Automated Software Analysis), 1999,6(1):69-95.
    [9] Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Robinet B, ed. Proc. of the 2nd Int’l Symp. on Programming. Paris, 1976. 106-130. http://www.di.ens.fr/～cousot/COUSOTpapers/ISOP76.shtml
    [10] Cousot P, Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Proc. of the 5th POPL. Arizona: ACM Press, 1978. 84-97.
    [11] Miné A. The octagon abstract domain. Higher-Order and Symbolic Computation, 2006,19(1):31-100.
    [12] Cousot P, Cousot R. Systematic design of program transformation frameworks. In: Launchbury J, Mitchell JC, eds. Proc. of the Symp. on Principles of Programming Languages. Portland: ACM Press, 2002. 178-190.
    [13] Cervesato I, Durgin N, Lincoln P, Mitchell J, Scedrov A. A metanotation for protocol analysis. In: Pandya P, Radhakrishnan J, eds. Proc. of the 12th IEEE Computer Security Foundation Workshop (CSFW-12). Mordano: IEEE, 1999. 55-69.
    [14] Blanchet B. An efficient cryptographic protocol verifier based on prolog rules. In: Pandya P, Radhakrishnan J, eds. Proc. of the 14th IEEE Computer Security Foundations Workshop. Cape Breton: IEEE Computer Society Press, 2001. 82-96.
    [15] Blanchet B. From secrecy to authenticity in security protocols. In: Cousot P, ed. Proc. of the 9th Int’l Static Analysis Symp. (SAS 2002). LNCS 2477, Madrid: Springer-Verlag, 2002. 342-359.
    [16] Goubaut-Larrecq J, Parrennes F. Cryptographic protocol analysis on real C code. In: Cousot R, ed. Proc. of the 6th Int’l Conf. on Verification, Model Checking and Abstract Interpretatio. LNCS 3385, Paris: Springer-Verlag, 2005. 363-379.
    [17] Bhargavan K, Fournet C, Gordon AD, Tse S. Verified interoperable implementations of security protocols. In: Proc. of the 19th IEEE Computer Security Foundations Workshop. Venice: IEEE Computer Society, 2006. 139-152. http://research.microsoft.com /～adg/Publications/tfng-csfw-2006.pdf
    [18] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. A static analyzer for large safety-critical software. In: Proc. of the ACMSIGPLAN 2003 Conf. PLDI. San Diego: ACM Press, 2003. 196-207.
    [19] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Mine A, Monniaux D, Rival X. Design and implementation of a special- purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen T, Schmidt D, Sudborough, eds. Proc. of the Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Jones ND. LNCS 2566, Springer-Verlag, 2002. 85-108.
    [20] Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X. The ASTRéE analyser. In: Sagiv M, ed. Proc. of the European Symp. on Programming. LNCS 3444, Edinburgh: Springer-Verlag, 2005. 21-30.
    [21] Mauborgne L. ASTRéE: Verification of absence of run-time error. In: Jacquard R, ed. Building the Information Society. Toulouse: Kluwer Academic Publishers, 2004. 385-392.
    [22] Mauborgne L, Rival X. Trace partitioning in abstract interpretation based static analyzer.In: Sagiv M, ed. Proc. of the European Symp. on Programming. LNCS 3444, Edinburgh: Springer-Verlag, 2005. 5-20.
    [23] Rival X. Understanding the origin of alarms in ASTRéE. In: Hankin C, Siveroni I, eds. Proc. of the 12th Int’l Static Analysis Symp. LNCS 3672, London: Springer-Verlag, 2005. 303-319.
    [24] Miné A. Field-Sensitive value analysis of embedded c programs with union types and pointer arithmetics. In: Irwin MJ, de Bosschere K, eds. Proc. of the Languages, Compilers, and Tools for Embedded Systems 2006 (LCTES). Ottawa: ACM Press, 2006. 54-63.
    [25] Graf S, Saidi H. Construction of abstract state graphs with PVS. In: Grumberg O, ed. Proc. of the CAV’97. LNCS 1254, Haifa: ACM Press, 1997. 72-83.
    [26] Colon M, Uribe TE. Generating finite state abstractions of reactive systems using decision procedures. In: Hu AJ, Vardi MY, eds. Proc. of the CAV’98. LNCS 1427, Vancouver: ACM Press, 1998. 293-304.
    [27] Das S, Dill D, Park S. Experience with predicate abstraction. In: Halbwachs N, Peled D, eds. Proc. of the 11th Int’l Conf. CAV’99. LNCS 1633, Trento: Springer-Verlag, 1999. 160-171.
    [28] Ball T, Rajamani SK. The SLAM project: Debugging system software via static analysis. In: Launchbury J, Mitchell JC, eds. Proc. of the Symp. on Principles of Programming Languages. Portland: ACM Press, 2002. 1-3.
    [29] Ball T, Naik M, Rajamani S. From symptom to cause: Localizing errors in counterexample traces. In: Bert D, Bowen JP, King S, Walden M. Proc. of the Symp. on Principles of Programming Languages. New Orleans: ACM Press, 2003. 97-105.
    [30] Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In: Launchbury J, Mitchell JC, eds. Proc. of the Symp. on Principles of Programming Languages. Portland: ACM Press, 2002. 58-70.
    [31] Henzinger TA, Jhala R, Majumdar R, McMillan KL. Abstractions from proofs. In: Jones ND, Leroy X, eds. Proc. of the 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Venice: ACM Press, 2004. 232-244.
    [32] Chaki S, Clarke EM, Groce A, Jha S, Veith H. Modular verification of software components in C. IEEE Trans. on Software Engineering, 2004,30(6):388-402.
    [33] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided abstraction refinement for symbolic model checking. Journal of the ACM, 2003,50(5):752-794.
    [34] Chaki S, Clarke E, Groce A, Ouaknine J, Yorav K. Efficient verification of sequential and concurrent C programs. Formal Methods in System Design, 2004,25(2-3):129-166.
    [35] Henzinger TA, Jhala R, Majumdar R, Qadeer S. Thread-Modular abstraction refinement. In: Jr Hunt WA, Somenzi F, eds. Proc. of the CAV 2003. Boulder: ACM Press, 2003. 262-274.
    [36] Qadeer S, Wu D. KISS: Keep it simple and seqeuential. In: Pugh W, Chambers C, eds. Proc. of the ACM SIGPLAN 2004 Conf. on Programming Language Design and Implementation. Washington: ACM Press, 2004. 14-24.
    [37] Podelski A, Rybalchenko A. Transition predicate abstraction and fair termination. In: Palsberg J, Abadi M, eds. Proc. of the Symp. on Principles of Programming Languages. ACM Press, 2005. 132-144.
    [38] Podelski A, Rybalchenko A. Transition invariants. In: Ganzinger H, ed. Proc. of the 9th Annual IEEE Symp. on. Logic in Computer Science. Turku: IEEE Computer Society Press, 2004. 32-41.
    [39] Cook B, Podelski A, Rybalchenko A. Abstraction refinement for termination. In: Hankin C, Siveroni I, eds. Proc. of the SAS 2005. LNCS 3672, London: Springer-Verlag, 2005. 87-101.
    [40] Cook B, Podelski A, Rybalchenko A. Terminator: Beyond safety. In: Ball T, Jones RB, eds. Proc. of the CAV 2006. LNCS 4144, Seattle: Springer-Verlag, 2006. 415-418.
    [41] Cook B, Podelski A, Rybalchenko A. Termination proofs for systems code. In: Schwartzbach MI, Ball T, eds. Proc. of the ACM SIGPLAN 2006 Conf. on Programming Language Design and Implementation. Ottawa: ACM Press, 2006.415-426.
    [42] Cook B, Gotsman A, Podelski A, Rybalchenko A, Vardi MY. Proving that programs eventually do something good. In: Hofmann M, Felleisen M, eds. Proc. of the Symp. on Principles of Programming Languages. Nice: ACM Press, 2007. 265-276.
    [43] Vardi MY. Verification of concurrent programs: The automata-theoretic framework. Annals of Pure and Applied Logic, 1991,51: 79-98.
    [44] Cousot P. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot R, ed. Proc. of the VMCAI 2005. LNCS 3385, Paris: Springer-Verlag, 2005. 1-24.
    [45] Rinetzky N, Bauer J, Reps T, Sagiv M, Wilhelm R. A semantics for procedure local heaps and its abstractions. In: Palsberg J, Abadi M, eds. Proc. of the Symp. on Principles of Programming Languages. ACM Press, 2005. 296-309.
    [46] Corbera F, Asenjo R, Zapata EL. A framework to capture dynamic data structures in pointer-based codes. IEEE Trans. on Parallel and Distributed Systems, 2004,15(2):151-166.
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

李梦君,李舟军,陈火旺.基于抽象解释理论的程序验证技术.软件学报,2008,19(1):17-26

复制
分享
文章指标
  • 点击次数:10864
  • 下载次数: 11995
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2006-11-14
  • 最后修改日期:2007-04-25
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19728422位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号