用于指针逻辑的自动定理证明器的设计与实现
|
摘要
对高可信软件需求的增加使得指针程序的验证成为近十几年的研究热点,自动定理证明作为形式化方法之一,在软件验证和程序分析工具当中发挥着及其重要的作用。然而,自动定理证明本身是一个非常难于解决的问题,尤其是待解决的问题中存在着指针以及涉及到指针的递归定义的谓词的情况下。
考虑到以上问题,我们在一个出具证明编译器框架中设计并实现了一个自动定理证明器和一个起辅助作用的证明检查器,来帮助完成指针程序的验证。实验结果证明,我们的实现不但具有创新性而且具有实际可行性。
在本文中,我们首先介绍了项目的研究背景和理论基础,然后提出了一种为指针逻辑来设计自动定理证明器的新技术,这项技术主要是基于变换和替代,我们已经在一个被称为APL的工具中实现了该技术。指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析。此外,本文还介绍了APL自动定理证明器的详细设计和实现,描述了一些关键算法,比如指针逻辑决策过程,整型线性算术决策过程,证明检查算法等等。APL定理证明器是完全自动的,并且APL所产生的证明可以被有效的记录和检查。在出具证明编译器PLCC 2中,我们调用了APL自动定理证明器,并对一些具有代表性的程序进行了测试。实验结果表明,APL完全可以自动地证明使用类C语言编写的关于单链表,双链表和二叉树的指针程序。
本文的主要特色和贡献为:
1.提出了一种为指针逻辑设计自动定理证明器的新方法。该方法是为了解决基于指针信息集合表示的验证条件的证明问题而设计的。在实现时我们使用了替代,变换,指针分析等基本技术,在指针信息集合上完成各种推理和证明。并且我们使用这种方法为指针逻辑实现了一个完全自动的定理证明器。这在已存在的比较流行的定理证明器中是不曾实现过的。
2.设计了指针逻辑的断言语言和相应的断言演算。该断言语言能够以简洁易懂的形式描述指针逻辑的最显著的特点,主要使用指针信息集合的形式表示待验证的指针程序在各程序点上的状态。断言语言和断言演算是定理证明器和证明检查器设计和实现的基础。
3.设计了一个证明检查算法,并在一个证明检查器中实现了该算法。该算法不同于已有的证明检查算法之处在于,它主要是使用模式匹配的方法对以指针信息集合表示为主的证明进行快速有效的检查,来保证证明的正确性。
4.实现了一个用于指针逻辑的自动定理证明器。该实现主要包含指针逻辑和整型线性算术两大理论的决策过程,独创的验证条件检查器,证明生成、保存和检查模块等。可以完全自动地证明出具证明编译器PLCC所产生的关于单链表,双链表和二叉树等程序实例的验证条件。APL自动定理证明器的实现,使得出具证明编译器PLCC 2不再需要依赖交互式证明工具Coq,能证明更多的、规模更大的程序实例,整个工具的功能因此变得更加强大。
The increasing demands for high-assurance software make the verification of pointer programs a hot research point over the past few years.Automated theorem proving is a method of the form methods,and it plays an important role in many software verification and program analysis tools.However,automated theorem proving is a difficult problem,particularly in the presence of pointers and recursively defined predicates involving pointers.
Taking all the problems mentioned above into account,we have designed and implemented an automated theorem prover and an auxiliary proof checker in the framework of a certifying compiler,the prover and checker are used to help accomplishing the verification of programs.The experimental results shows our implementation not only new but also practical.
In this paper,we first introduce the research background and theory foundation of the project.Then we present a new technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic,and we have implemented this technique in a tool called APL.As an extension of Hoare logic, Pointer Logic can be used for accurate pointer analysis of pointer programs. Furthermore,this paper introduces some details in designing and implementing of the APL automated theorem prover for Pointer Logic,and describes some algorithms.For example,the decision procedures for Pointer Logic,the decision procedures for linear integer arithmetic,the proof checking algorithm and so on.The APL theorem prover is fully automated and proofs can be recorded and checked efficiently.We invoked the APL theorem prover in the certifying compiler PLCC and tested some representative programs.The experimental results show our implementation can fully automatically prove the verification conditions for pointer programs in C-like language and produce machine-checkable proofs.The programs for testing are mainly about singly-linked lists,doubly-linked lists and binary trees.
The main contributions and features of this thesis are:
1.It presents a new method for designing automated theorem provers for Pointer Logic.This method is designed for proving the verification conditions using pointer information set as its basic form.When implementing,we used some techniques,such as substitute-ion,transformation and pointer analysis,and accomplish reasoning and proving on the pointer information set.We have implemented an automated theorem prover using this method,and we are the first to do so.
2.It designs the assertion language and assertion calculus for Pointer Logic.The assertion language can describe the most distinct characters of the Pointer Logic in a compact and pellucid way.The language use the pointer information set to present the state of the program being verified on each point.The assertion language and the corresponding assertion calculus are the basis for designing and implementing the prover and checker.
3.It designs a proof checking algorithm,and has implemented this algorithm in a proof checker.The difference between this algorithm and other existing ones is,it use pattern matching to finish proof checking effciently for the proof using pointer information set as its main form,to assure the correctness of the proof.
4.It implements an automated theorem prover for Pointer Logic.The implementaion mainly contains the decision procedure of Pointer Logic,the decision procedure of linear integer arithmetic,a unique verification condition checker,proof generation,proof recording,and proof checking and so on.It can automatically prove the verification conditions generated by the PLCC certifying complier for programs about singly-linked list,doubly-linked list and trees.The implementation of APL theorem prover makes the PLCC no longer need to depend on the proof assistant Coq, and can proof more complicated programs;the capability of the whole tool has been improved.
考虑到以上问题,我们在一个出具证明编译器框架中设计并实现了一个自动定理证明器和一个起辅助作用的证明检查器,来帮助完成指针程序的验证。实验结果证明,我们的实现不但具有创新性而且具有实际可行性。
在本文中,我们首先介绍了项目的研究背景和理论基础,然后提出了一种为指针逻辑来设计自动定理证明器的新技术,这项技术主要是基于变换和替代,我们已经在一个被称为APL的工具中实现了该技术。指针逻辑作为Hoare逻辑的扩展,可以对指针程序进行精确的分析。此外,本文还介绍了APL自动定理证明器的详细设计和实现,描述了一些关键算法,比如指针逻辑决策过程,整型线性算术决策过程,证明检查算法等等。APL定理证明器是完全自动的,并且APL所产生的证明可以被有效的记录和检查。在出具证明编译器PLCC 2中,我们调用了APL自动定理证明器,并对一些具有代表性的程序进行了测试。实验结果表明,APL完全可以自动地证明使用类C语言编写的关于单链表,双链表和二叉树的指针程序。
本文的主要特色和贡献为:
1.提出了一种为指针逻辑设计自动定理证明器的新方法。该方法是为了解决基于指针信息集合表示的验证条件的证明问题而设计的。在实现时我们使用了替代,变换,指针分析等基本技术,在指针信息集合上完成各种推理和证明。并且我们使用这种方法为指针逻辑实现了一个完全自动的定理证明器。这在已存在的比较流行的定理证明器中是不曾实现过的。
2.设计了指针逻辑的断言语言和相应的断言演算。该断言语言能够以简洁易懂的形式描述指针逻辑的最显著的特点,主要使用指针信息集合的形式表示待验证的指针程序在各程序点上的状态。断言语言和断言演算是定理证明器和证明检查器设计和实现的基础。
3.设计了一个证明检查算法,并在一个证明检查器中实现了该算法。该算法不同于已有的证明检查算法之处在于,它主要是使用模式匹配的方法对以指针信息集合表示为主的证明进行快速有效的检查,来保证证明的正确性。
4.实现了一个用于指针逻辑的自动定理证明器。该实现主要包含指针逻辑和整型线性算术两大理论的决策过程,独创的验证条件检查器,证明生成、保存和检查模块等。可以完全自动地证明出具证明编译器PLCC所产生的关于单链表,双链表和二叉树等程序实例的验证条件。APL自动定理证明器的实现,使得出具证明编译器PLCC 2不再需要依赖交互式证明工具Coq,能证明更多的、规模更大的程序实例,整个工具的功能因此变得更加强大。
The increasing demands for high-assurance software make the verification of pointer programs a hot research point over the past few years.Automated theorem proving is a method of the form methods,and it plays an important role in many software verification and program analysis tools.However,automated theorem proving is a difficult problem,particularly in the presence of pointers and recursively defined predicates involving pointers.
Taking all the problems mentioned above into account,we have designed and implemented an automated theorem prover and an auxiliary proof checker in the framework of a certifying compiler,the prover and checker are used to help accomplishing the verification of programs.The experimental results shows our implementation not only new but also practical.
In this paper,we first introduce the research background and theory foundation of the project.Then we present a new technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic,and we have implemented this technique in a tool called APL.As an extension of Hoare logic, Pointer Logic can be used for accurate pointer analysis of pointer programs. Furthermore,this paper introduces some details in designing and implementing of the APL automated theorem prover for Pointer Logic,and describes some algorithms.For example,the decision procedures for Pointer Logic,the decision procedures for linear integer arithmetic,the proof checking algorithm and so on.The APL theorem prover is fully automated and proofs can be recorded and checked efficiently.We invoked the APL theorem prover in the certifying compiler PLCC and tested some representative programs.The experimental results show our implementation can fully automatically prove the verification conditions for pointer programs in C-like language and produce machine-checkable proofs.The programs for testing are mainly about singly-linked lists,doubly-linked lists and binary trees.
The main contributions and features of this thesis are:
1.It presents a new method for designing automated theorem provers for Pointer Logic.This method is designed for proving the verification conditions using pointer information set as its basic form.When implementing,we used some techniques,such as substitute-ion,transformation and pointer analysis,and accomplish reasoning and proving on the pointer information set.We have implemented an automated theorem prover using this method,and we are the first to do so.
2.It designs the assertion language and assertion calculus for Pointer Logic.The assertion language can describe the most distinct characters of the Pointer Logic in a compact and pellucid way.The language use the pointer information set to present the state of the program being verified on each point.The assertion language and the corresponding assertion calculus are the basis for designing and implementing the prover and checker.
3.It designs a proof checking algorithm,and has implemented this algorithm in a proof checker.The difference between this algorithm and other existing ones is,it use pattern matching to finish proof checking effciently for the proof using pointer information set as its main form,to assure the correctness of the proof.
4.It implements an automated theorem prover for Pointer Logic.The implementaion mainly contains the decision procedure of Pointer Logic,the decision procedure of linear integer arithmetic,a unique verification condition checker,proof generation,proof recording,and proof checking and so on.It can automatically prove the verification conditions generated by the PLCC certifying complier for programs about singly-linked list,doubly-linked list and trees.The implementation of APL theorem prover makes the PLCC no longer need to depend on the proof assistant Coq, and can proof more complicated programs;the capability of the whole tool has been improved.
引文
[1]R.W.Butler.What is formal methods[N/OL].http://shemesh.larc.nasa.gov/fm/fm-what.html Retrieved on 2009.
[2]John C.Reynolds.Separation logic:a logic for shared mutable data structures.In the 17~(th)Annual IEEE Symposium on Logic in Computer Science.Pages 55-74,July 2002.
[3]Josh Berdine,Cristiano Calcagno,and Peter W.O'Heam.Smallfoot:modular automatic ass -ertion checking with separation logic.In International Symposium on Formal Methods for Components and Objects,volume 4111 of Lecture Notes in Computer Science,pages 115-137,2005.
[4]M.Sagiv,T.Reps,and R.Wilhelm.Solving shape-analysis problems in languages with dest -ructtive updating.ACM TOPLAS,20(1):1-5,1998.
[5]M.Sagiv,T.Reps,and R.Wilhelm.Parametric shape analysis via 3valued logic.ACM Trans.Program.Lang.Syst.,24(3):217-298,2002.
[6]A.M鰈ler and M.I.Schwartzbach.The pointer assertion logic engine.In 8th PLDI,page 221-231,2001.
[7]A.M鲽ler.PALE project home page.www.brics.dk/PALE.Retrieved on 2009.
[8]Nils Klarlund and Michael I.Schwartzbach.Graph types.In Principles of Programming Languages,POPL,1993.
[9]Geoff Sutcliffe.Overview of automated theorem proving,http://www.cs.miami.edu/-tptp/OverviewOfATP.html.Retrieved on 2009.
[10]Allen,Stuart F.,Robert L.,Constable,Richard Eaton,Christoph Kreitz,Lori Lorigo.The Nuprl open logical environment.Proceedings of 17th International Conference on Autom -ated Deduction,LNAI 1831,Springer-Verlag,2000.170-176.
[11]L.C.Paulson,T.Nipkow.Isabelle:a generic theorem prover,volume 828 of Lecture Notes in Computer Science.Springer-Verlag Berlin,1994.
[12]L.C.Paulson.The Isabelle reference manual.Technical Report 283,University of Cambri -dge Computer Laboratory,1997.
[13]S.Owre,J.M.Rushby,N.Shankar.PVS:a prototype verification system.In 11th Internati -onal Conference on Automated Deduction(CADE),Deepak Kapur,ED.,Saratoga,NY,1992.748-752.
[14]The Coq Development Team.The Coq proof assistant reference manual.The Coq release v7.1,2001.
[15]Matt Kaufmann,J Strother Moore.Design goals for ACL2.In proceedings of:Third Interna-tional School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems,Kiel,Germany.Published by Christian-Albrechts-Universitat,1994.92-117.
[16]Automated Reasoning Group.HOL page http://www.cl.cam.ac.uk/research/hvg/HOL/.
[17]M.J.C.Gordon and T.F.Melham.Introduction to HOL:a theorem proving environment for higher order logic.Cambridge University Press,1993.
[18]L.C.Paulson.ML for the working programmer(2nd edition).Cambridge University Press,1996.
[19]Milner,R.,Logic for computable functions,description of a machine implementation.Artificial Intelligence Memo No.169,Stanford University,1972.
[20]Aiello,L.and Aiello,M.,Proving program correctness in LCF.The Colloquium on Programming,Paris,9-1,1974.
[21]D.Lie,C.A.Thekkath,and M.Horowitz.Implementing an unrrusted operating system on trusted hardware.In Proceedings of the nineteenth ACM symposium on Operating systems principles,pp.178-192,ACM Press,2003.
[22]Edmund M.Clarke,Jr.,Orna Grumberg,and Doron A.Peled.Model checking.MIT Press,1999.
[23]B.Berard,M.Bidoit,A.Finkel,F.Laroussinie,A.Petit,L.Petrucci,and P.Schnoebelen,Sy stems and software verification:model-checking techniques and tools.Vuibert,Paris,1999.
[24]Michael Huth and Mark Ryan.Logic in computer science:modelling and reasoning about Systems.Cambridge University Press,2004.
[25]M黮ler-Olm,M.,Schmidt,D.A.and Steffen,B.Model checking:a tutorial introduction.Proc.6th Static Analysis Symposium,G.File and A.Cortesi,eds.,Springer LNCS 1694,pp.330-354.1999.
[26]Michael Huth and Mark Ryan.Logic in computer science(2nd edition).Cambridge University Press,pp.207.2004.
[27]Emerson,E.A.and Halpern,J.Y.,Decision procedures and expressiveness in the temporal logic of branching time.Journal of Computer and System Sciences 30(1):1-24.1985.
[28]Emerson,E.A..Temporal and modal logic,in J.van Leeuwen(ed.).Handbook of Theoretical Computer Science,vol.B.MIT Press,pp.955-1072.1990.
[29]Sheldon B.Akers.Binary decision diagrams,IEEE Transactions on Computers,C-27(6):509-516,1978.
[30]Karl S.Brace,Richard L.Rudell and Randal E.Bryant.“Efficient Implementation of a BDD Package”.In Proceedings of the 27th ACM/IEEE Design Automation Conference,pp.40-45. IEEE Computer Society Press,1990.
[31]Holzmann,G.J.,The SPIN model checker:primer and reference manual.Addison-Wesley,2004.
[32]BLAST Homepage,http://mtc.epfl.ch/software-tools/blast/
[33]Dirk Beyer,Thomas A.Henzinger,Ranjit Jhala,and Rupak Majumdar.The software model checker Blast.International Journal on Software Tools for Technology Transfer(STTT),9(5-6):505-525,2007.
[34]Thomas A.Henzinger,Ranjit Jhala,Rupak Majumdar,and Gregoire Sutre.Software verification with Blast.In Proceedings of the 10th SPIN Workshop on Model Checking Software(SPIN 2003),LNCS 2648,Springer-Verlag,pp.235-239,2003.
[35]Hongseok Yang.Local reasoning for stateful programs.Ph.D.dissertation,University of Illinois,Urbana-Champaign,Illinois,2001.
[36]Hongseok Yang.An example of local reasoning in BI pointer logic:The Schorr-Waite graph marking algorithm.In Fritz Henglein,John Hughes,Henning Makholm,and Henning Niss,editors,SPACE 2001:Informal Proceedings of Workshop on Semantics,Program Analysis and Computing Environments for Memory Management,pp.41-68.IT University of Copenhagen.2001.
[37]Lars Birkedal,Noah Torp-Smith,and John C.Reynolds.Local reasoning about a copying garbage collector.2008.
[38]Cristiano Calcagno,Hongseok Yang,and Peter W.O'Hearn.Computability and complexity results for a spatial assertion language for data structures.In Ramesh Hariharan,Madhavan Mukund,and V.Vinay,editors,FST TCS 2001:Foundations of Software Technology and Theoretical Computer Science,volume 2245 of Lecture Notes in Computer Science,pp.108-119,Berlin,2001.Springer-Verlag.
[39]John C.Reynolds.Separation logic:A logic for shared mutable data structures.In Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science,pp.55-74,Los Alamitos,California,2002.IEEE Computer Society.
[40]Josh Berdine,Cristiano Calcagno,and Peter W.O'Hearn.A decidable fragment of separation logic.In Kamal Lodaya and Meena Mahajan,editors,FSTTCS 2004:Foundations of Software Technology and Theoretical Computer Science,volume 3328 of Lecture Notes in Computer Science,pp.97-109,Berlin,2004.Springer-Verlag.
[41]Bodil Biering,Lars Birkedal,and Noah Torp-Smith.Bi-hyperdoctrines and higher order separation logic.In Proceedings of ESOP 2005:The European Symposium on Programming,pp.233-247,2005.
[42]Carsten Vanning and Lars Birkedal.Higher-order separation logic in Isabelle/HOL.To appear in the Proceedings of the 24th Annual Conference on Mathematical Foundations of Programming Semantics,Electronic Notes in Theoretical Computer Science,2008.
[43]Dachuan Yu,Nadeem A.Hamid,and Zhong Shao.Building certified libraries for PCC:Dynamic storage allocation.Science of Computer Programming,50:101-127,2004.
[44]A.M鲽ler and M.I.Schwartzbach.The pointer assertion logic engine[C],In 8th PLDI,pp.221-231,2001.
[45]A.M鲽ler.PALE project home page[EB/OL].http://www.brics.dk/PALE.
[46]Nils Klarlund.Mona & Fido:The logic-automaton connection in practice.In Computer Science Logic,CSL'97,volume 1414 of LNCS,1998.
[47]Nils Klarlund and Anders M_ller.MONA Version 1.4 User Manual.BRICS Notes Series NS-01-1,Department of Computer Science,University of Aarhus,2001.
[48]Anders M(烏代)ler.MONA project home page,www.brics.dk/mona.
[49]T.Hoare.The verifying compiler:a grand challenge for computing research.J.of ACM,50(1),pp.63-69,2003.
[50]G.C.Necula:Proof Carrying Code.In Conference Record of the 24th Symposium on Principles of Programming Languages(POPL.97),1997.
[51]G.C.Necula,P.Lee:The Design and Implementation of a Certifying Compiler.In Proceedings of the Conference on Programming Language Design and Implementation.1998.
[52]C.Colby et.al.:A Certifying Compiler for Java.In Proceedings of the Conference on Programming Language Design and Implementation(PLDI.00).2000.
[53]Yiyun Chen,Lin Ge,Baojian Hua,Zhaopeng Li,Cheng Liu.Design of a certifying compiler supporting proof of program safety.TASE,First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering(TASE '07),pp.127-138.2007.
[54]Yiyun Chen,Lin Ge,Baojian Hua,Zhaopeng Li,Cheng Liu,and Zhifang Wang.A pointer logic and certifying compiler.Frontiers of Computer Science in China,1(3):297-312.2007.
[55]Wang Zhifang,Chen Yiyun,Wang Zhenming,Hua Baojian.Automated verification of pointer pPrograms in pointer logic.Frontiers of Computer Science in China,2(4),pp.380-397.2008.
[56]Wang Zhifang,Chen Yiyun,Wang Zhenming,Wang Wei and Tian Bo.Implementation of pointer pogic for automated verification.In Proceedings of 1~(st)International Symposium on Trusted Computing(TrustCom08),pp.2295-2301,Zhangjiajie,China,Nov.2008.
[57]Wang Zhifang,Chen Yiyun,Wang Zhenming,Wang Wei and Tian Bo.An extension to pointer lLogic for verification.In Proceedings of 2nd IEEE &IFIP International Symposium on Theoretical Aspects of Software Engineering(TASE08),pp.49-56,Nanjing,China,2008.
[58]Yiyun Chen,Baojian Hua,Lin Ge,et al.A pointer logic for safety verification of pointer programs[K].Chinese Journal of Computers,31(3):372-380,2008.
[59]B.Hua,L.Ge.The definition of PointerC programming language,http://ssg.ustcsz.edu.cn/lss/doc/index.html.
[60]E.W.Dijkstra.A discipline of programming.Englewood Cliffs.Prentice Hall,1976.
[61]R.W.Floyd,Assigning meanings to programs.In Mathematical Aspects of Computer Science(J.T.Schwartz,ed.),vol.19 of Proceedings of Symposia in Applied Mathematics,pp.19-32,American Mathematical Society,1967.
[62]C.A.R.Hoare,An axiomatic basis for computer programming,Communications ACM,vol.12,no.10,pp.576-580,1969.
[63]Baojian Hua,Yiyun Chen,Zhaopeng Li,Zhifang Wang,and Lin Ge.Design and proof of a safe programming language PointerC.Chinese Journal of Computers,31(4):556-564,April 2008.
[64]Standard ML of New Jersy homepage,http://www.smlnj.org/.
[65]The Caml homepage,http://caml.inria.fr/.
[66]D.C.Cooper.Theorem proving in arithmetic with multiplication.In B.Meltzer and D.Michie,editors,Machine Intelligence 7,pp.91-99.American Elsevier,New York,1972.
[67]Reddy,C.R.,and D.W.Loveland,Presburger arithmetic with bounded quantifier alternation.ACM Symposium on Theory of Computing:320-325,1978.
[68]Alexander Schrijver,Theory of Linear and Integer Programming.John Wiley & sons,pp.155-156,1998.
[69]Greenberg,Harvey J.,Klee-Minty polytope shows exponential time complexity of simplex method.University of Colorado at Denver,1997.
[70]Spyros Reveliotis.An introduction to linear programming and the Simplex algorithm.The Georgia Institute of Technology.http://www2.isye.gatech.edu/～spyros/LP/ LP.html
[71]The Omega Project homepage,http://www.cs.umd.edu/projects/omega/
[72]Pugh,William,The Omega test:a fast and practical integer programming algorithm for dependence analysis.Communications of the ACM.pp.4-13,1991.
[73]Greg Nelson,Derek C.Oppen.Fast decision procedures based on congruence closure.J.of ACM 27(2):356-364,1980.
[74]W.Wong.Recording HOL proofs.TR.306,University of Cambridge Computer Laboratory,New Museums Site,Pembroke Street,Cambridge CB 23 QG,England,1993.
[75]W.Wong.A proof checker for HOL.TR.389,University of Cambridge Computer Laboratory,New Museums Site,Pembroke Street,Cambridge CB 23 QG,England,1996.
[76]W.Wong.Recording and checking HOL proofs.In E.T.Schubert,P.J.Windley,and J.Alves-Foss,editors,Higher-Order Logic Theorem Proving and Its Applications,Lecture Notes in Computer Science.Springer-Verlag,971:353-368,1995.
[77]Geoffrey Norman Watson.Proof representation in theorem provers.Technical Report 98-13,Software Verification Centre,School of Informatics Technology,The University of Queensland,Queensland 4072,Australia,1998.
[78]Appel,A.W,Michael,N.,Stump,A.,and Virga,R.A trustworthy proof checker.J.Autom.Reason.31,3-4(Jan.2004),231-260.
[79]Watson and Geoffrey Norman.A generic proof checker.PhD thesis,2001.
[2]John C.Reynolds.Separation logic:a logic for shared mutable data structures.In the 17~(th)Annual IEEE Symposium on Logic in Computer Science.Pages 55-74,July 2002.
[3]Josh Berdine,Cristiano Calcagno,and Peter W.O'Heam.Smallfoot:modular automatic ass -ertion checking with separation logic.In International Symposium on Formal Methods for Components and Objects,volume 4111 of Lecture Notes in Computer Science,pages 115-137,2005.
[4]M.Sagiv,T.Reps,and R.Wilhelm.Solving shape-analysis problems in languages with dest -ructtive updating.ACM TOPLAS,20(1):1-5,1998.
[5]M.Sagiv,T.Reps,and R.Wilhelm.Parametric shape analysis via 3valued logic.ACM Trans.Program.Lang.Syst.,24(3):217-298,2002.
[6]A.M鰈ler and M.I.Schwartzbach.The pointer assertion logic engine.In 8th PLDI,page 221-231,2001.
[7]A.M鲽ler.PALE project home page.www.brics.dk/PALE.Retrieved on 2009.
[8]Nils Klarlund and Michael I.Schwartzbach.Graph types.In Principles of Programming Languages,POPL,1993.
[9]Geoff Sutcliffe.Overview of automated theorem proving,http://www.cs.miami.edu/-tptp/OverviewOfATP.html.Retrieved on 2009.
[10]Allen,Stuart F.,Robert L.,Constable,Richard Eaton,Christoph Kreitz,Lori Lorigo.The Nuprl open logical environment.Proceedings of 17th International Conference on Autom -ated Deduction,LNAI 1831,Springer-Verlag,2000.170-176.
[11]L.C.Paulson,T.Nipkow.Isabelle:a generic theorem prover,volume 828 of Lecture Notes in Computer Science.Springer-Verlag Berlin,1994.
[12]L.C.Paulson.The Isabelle reference manual.Technical Report 283,University of Cambri -dge Computer Laboratory,1997.
[13]S.Owre,J.M.Rushby,N.Shankar.PVS:a prototype verification system.In 11th Internati -onal Conference on Automated Deduction(CADE),Deepak Kapur,ED.,Saratoga,NY,1992.748-752.
[14]The Coq Development Team.The Coq proof assistant reference manual.The Coq release v7.1,2001.
[15]Matt Kaufmann,J Strother Moore.Design goals for ACL2.In proceedings of:Third Interna-tional School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems,Kiel,Germany.Published by Christian-Albrechts-Universitat,1994.92-117.
[16]Automated Reasoning Group.HOL page http://www.cl.cam.ac.uk/research/hvg/HOL/.
[17]M.J.C.Gordon and T.F.Melham.Introduction to HOL:a theorem proving environment for higher order logic.Cambridge University Press,1993.
[18]L.C.Paulson.ML for the working programmer(2nd edition).Cambridge University Press,1996.
[19]Milner,R.,Logic for computable functions,description of a machine implementation.Artificial Intelligence Memo No.169,Stanford University,1972.
[20]Aiello,L.and Aiello,M.,Proving program correctness in LCF.The Colloquium on Programming,Paris,9-1,1974.
[21]D.Lie,C.A.Thekkath,and M.Horowitz.Implementing an unrrusted operating system on trusted hardware.In Proceedings of the nineteenth ACM symposium on Operating systems principles,pp.178-192,ACM Press,2003.
[22]Edmund M.Clarke,Jr.,Orna Grumberg,and Doron A.Peled.Model checking.MIT Press,1999.
[23]B.Berard,M.Bidoit,A.Finkel,F.Laroussinie,A.Petit,L.Petrucci,and P.Schnoebelen,Sy stems and software verification:model-checking techniques and tools.Vuibert,Paris,1999.
[24]Michael Huth and Mark Ryan.Logic in computer science:modelling and reasoning about Systems.Cambridge University Press,2004.
[25]M黮ler-Olm,M.,Schmidt,D.A.and Steffen,B.Model checking:a tutorial introduction.Proc.6th Static Analysis Symposium,G.File and A.Cortesi,eds.,Springer LNCS 1694,pp.330-354.1999.
[26]Michael Huth and Mark Ryan.Logic in computer science(2nd edition).Cambridge University Press,pp.207.2004.
[27]Emerson,E.A.and Halpern,J.Y.,Decision procedures and expressiveness in the temporal logic of branching time.Journal of Computer and System Sciences 30(1):1-24.1985.
[28]Emerson,E.A..Temporal and modal logic,in J.van Leeuwen(ed.).Handbook of Theoretical Computer Science,vol.B.MIT Press,pp.955-1072.1990.
[29]Sheldon B.Akers.Binary decision diagrams,IEEE Transactions on Computers,C-27(6):509-516,1978.
[30]Karl S.Brace,Richard L.Rudell and Randal E.Bryant.“Efficient Implementation of a BDD Package”.In Proceedings of the 27th ACM/IEEE Design Automation Conference,pp.40-45. IEEE Computer Society Press,1990.
[31]Holzmann,G.J.,The SPIN model checker:primer and reference manual.Addison-Wesley,2004.
[32]BLAST Homepage,http://mtc.epfl.ch/software-tools/blast/
[33]Dirk Beyer,Thomas A.Henzinger,Ranjit Jhala,and Rupak Majumdar.The software model checker Blast.International Journal on Software Tools for Technology Transfer(STTT),9(5-6):505-525,2007.
[34]Thomas A.Henzinger,Ranjit Jhala,Rupak Majumdar,and Gregoire Sutre.Software verification with Blast.In Proceedings of the 10th SPIN Workshop on Model Checking Software(SPIN 2003),LNCS 2648,Springer-Verlag,pp.235-239,2003.
[35]Hongseok Yang.Local reasoning for stateful programs.Ph.D.dissertation,University of Illinois,Urbana-Champaign,Illinois,2001.
[36]Hongseok Yang.An example of local reasoning in BI pointer logic:The Schorr-Waite graph marking algorithm.In Fritz Henglein,John Hughes,Henning Makholm,and Henning Niss,editors,SPACE 2001:Informal Proceedings of Workshop on Semantics,Program Analysis and Computing Environments for Memory Management,pp.41-68.IT University of Copenhagen.2001.
[37]Lars Birkedal,Noah Torp-Smith,and John C.Reynolds.Local reasoning about a copying garbage collector.2008.
[38]Cristiano Calcagno,Hongseok Yang,and Peter W.O'Hearn.Computability and complexity results for a spatial assertion language for data structures.In Ramesh Hariharan,Madhavan Mukund,and V.Vinay,editors,FST TCS 2001:Foundations of Software Technology and Theoretical Computer Science,volume 2245 of Lecture Notes in Computer Science,pp.108-119,Berlin,2001.Springer-Verlag.
[39]John C.Reynolds.Separation logic:A logic for shared mutable data structures.In Proceedings Seventeenth Annual IEEE Symposium on Logic in Computer Science,pp.55-74,Los Alamitos,California,2002.IEEE Computer Society.
[40]Josh Berdine,Cristiano Calcagno,and Peter W.O'Hearn.A decidable fragment of separation logic.In Kamal Lodaya and Meena Mahajan,editors,FSTTCS 2004:Foundations of Software Technology and Theoretical Computer Science,volume 3328 of Lecture Notes in Computer Science,pp.97-109,Berlin,2004.Springer-Verlag.
[41]Bodil Biering,Lars Birkedal,and Noah Torp-Smith.Bi-hyperdoctrines and higher order separation logic.In Proceedings of ESOP 2005:The European Symposium on Programming,pp.233-247,2005.
[42]Carsten Vanning and Lars Birkedal.Higher-order separation logic in Isabelle/HOL.To appear in the Proceedings of the 24th Annual Conference on Mathematical Foundations of Programming Semantics,Electronic Notes in Theoretical Computer Science,2008.
[43]Dachuan Yu,Nadeem A.Hamid,and Zhong Shao.Building certified libraries for PCC:Dynamic storage allocation.Science of Computer Programming,50:101-127,2004.
[44]A.M鲽ler and M.I.Schwartzbach.The pointer assertion logic engine[C],In 8th PLDI,pp.221-231,2001.
[45]A.M鲽ler.PALE project home page[EB/OL].http://www.brics.dk/PALE.
[46]Nils Klarlund.Mona & Fido:The logic-automaton connection in practice.In Computer Science Logic,CSL'97,volume 1414 of LNCS,1998.
[47]Nils Klarlund and Anders M_ller.MONA Version 1.4 User Manual.BRICS Notes Series NS-01-1,Department of Computer Science,University of Aarhus,2001.
[48]Anders M(烏代)ler.MONA project home page,www.brics.dk/mona.
[49]T.Hoare.The verifying compiler:a grand challenge for computing research.J.of ACM,50(1),pp.63-69,2003.
[50]G.C.Necula:Proof Carrying Code.In Conference Record of the 24th Symposium on Principles of Programming Languages(POPL.97),1997.
[51]G.C.Necula,P.Lee:The Design and Implementation of a Certifying Compiler.In Proceedings of the Conference on Programming Language Design and Implementation.1998.
[52]C.Colby et.al.:A Certifying Compiler for Java.In Proceedings of the Conference on Programming Language Design and Implementation(PLDI.00).2000.
[53]Yiyun Chen,Lin Ge,Baojian Hua,Zhaopeng Li,Cheng Liu.Design of a certifying compiler supporting proof of program safety.TASE,First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering(TASE '07),pp.127-138.2007.
[54]Yiyun Chen,Lin Ge,Baojian Hua,Zhaopeng Li,Cheng Liu,and Zhifang Wang.A pointer logic and certifying compiler.Frontiers of Computer Science in China,1(3):297-312.2007.
[55]Wang Zhifang,Chen Yiyun,Wang Zhenming,Hua Baojian.Automated verification of pointer pPrograms in pointer logic.Frontiers of Computer Science in China,2(4),pp.380-397.2008.
[56]Wang Zhifang,Chen Yiyun,Wang Zhenming,Wang Wei and Tian Bo.Implementation of pointer pogic for automated verification.In Proceedings of 1~(st)International Symposium on Trusted Computing(TrustCom08),pp.2295-2301,Zhangjiajie,China,Nov.2008.
[57]Wang Zhifang,Chen Yiyun,Wang Zhenming,Wang Wei and Tian Bo.An extension to pointer lLogic for verification.In Proceedings of 2nd IEEE &IFIP International Symposium on Theoretical Aspects of Software Engineering(TASE08),pp.49-56,Nanjing,China,2008.
[58]Yiyun Chen,Baojian Hua,Lin Ge,et al.A pointer logic for safety verification of pointer programs[K].Chinese Journal of Computers,31(3):372-380,2008.
[59]B.Hua,L.Ge.The definition of PointerC programming language,http://ssg.ustcsz.edu.cn/lss/doc/index.html.
[60]E.W.Dijkstra.A discipline of programming.Englewood Cliffs.Prentice Hall,1976.
[61]R.W.Floyd,Assigning meanings to programs.In Mathematical Aspects of Computer Science(J.T.Schwartz,ed.),vol.19 of Proceedings of Symposia in Applied Mathematics,pp.19-32,American Mathematical Society,1967.
[62]C.A.R.Hoare,An axiomatic basis for computer programming,Communications ACM,vol.12,no.10,pp.576-580,1969.
[63]Baojian Hua,Yiyun Chen,Zhaopeng Li,Zhifang Wang,and Lin Ge.Design and proof of a safe programming language PointerC.Chinese Journal of Computers,31(4):556-564,April 2008.
[64]Standard ML of New Jersy homepage,http://www.smlnj.org/.
[65]The Caml homepage,http://caml.inria.fr/.
[66]D.C.Cooper.Theorem proving in arithmetic with multiplication.In B.Meltzer and D.Michie,editors,Machine Intelligence 7,pp.91-99.American Elsevier,New York,1972.
[67]Reddy,C.R.,and D.W.Loveland,Presburger arithmetic with bounded quantifier alternation.ACM Symposium on Theory of Computing:320-325,1978.
[68]Alexander Schrijver,Theory of Linear and Integer Programming.John Wiley & sons,pp.155-156,1998.
[69]Greenberg,Harvey J.,Klee-Minty polytope shows exponential time complexity of simplex method.University of Colorado at Denver,1997.
[70]Spyros Reveliotis.An introduction to linear programming and the Simplex algorithm.The Georgia Institute of Technology.http://www2.isye.gatech.edu/～spyros/LP/ LP.html
[71]The Omega Project homepage,http://www.cs.umd.edu/projects/omega/
[72]Pugh,William,The Omega test:a fast and practical integer programming algorithm for dependence analysis.Communications of the ACM.pp.4-13,1991.
[73]Greg Nelson,Derek C.Oppen.Fast decision procedures based on congruence closure.J.of ACM 27(2):356-364,1980.
[74]W.Wong.Recording HOL proofs.TR.306,University of Cambridge Computer Laboratory,New Museums Site,Pembroke Street,Cambridge CB 23 QG,England,1993.
[75]W.Wong.A proof checker for HOL.TR.389,University of Cambridge Computer Laboratory,New Museums Site,Pembroke Street,Cambridge CB 23 QG,England,1996.
[76]W.Wong.Recording and checking HOL proofs.In E.T.Schubert,P.J.Windley,and J.Alves-Foss,editors,Higher-Order Logic Theorem Proving and Its Applications,Lecture Notes in Computer Science.Springer-Verlag,971:353-368,1995.
[77]Geoffrey Norman Watson.Proof representation in theorem provers.Technical Report 98-13,Software Verification Centre,School of Informatics Technology,The University of Queensland,Queensland 4072,Australia,1998.
[78]Appel,A.W,Michael,N.,Stump,A.,and Virga,R.A trustworthy proof checker.J.Autom.Reason.31,3-4(Jan.2004),231-260.
[79]Watson and Geoffrey Norman.A generic proof checker.PhD thesis,2001.