基于携带证明的代码的垃圾收集过程验证
|
摘要
使用Java和C#等安全的程序设计语言编写的程序能够完全避免一些在传统程序设计语言编写的程序中经常出现的安全漏洞,从而提高软件的可靠性。然而,这类安全语言的众多安全特性都依赖于其运行环境,特别是垃圾收集机制的正确性和安全性。不幸的是,垃圾收集算法通常难于设计和正确地实现。同时,垃圾收集器和用户程序的交互过程也往往相当复杂而易出错。因此,为了提高使用垃圾收集机制的程序设计语言的安全性和可靠性,势必需要对垃圾收集过程的安全性和正确性进行严格的研究。
本文工作使用基于Hoare逻辑的汇编语言级形式程序验证框架,对垃圾收集器的安全性和正确性,以及垃圾收集器与多种用户程序,特别是类型化汇编语言的交互过程的安全性进行了严格的形式验证。本文工作基于携带证明的代码技术,所有的验证都在计算机辅助定理证明工具COQ中实现为计算机可检查的证明。这样,垃圾收集器和用户程序就能够被构造为一个完整的携带安全性证明的软件包,方便地通过互联网和其他渠道进行发布。
本文的第一部分工作验证了两种典型垃圾收集器的汇编语言实现。该工作使用分离逻辑风格的代码规范语言给出了停止式标记—清扫垃圾收集器和基于初始快照的Yuasa渐进式垃圾收集器的安全规范,并使用Hoare风格的程序逻辑和推理方法证明了垃圾收集器满足其安全规范。
第二部分工作从单独验证垃圾收集器工作存在的不足出发,提出并实现了一种通用的验证垃圾收集器和用户程序交互过程的方法。其核心思想是使用类似抽象数据类型的技术将垃圾收集器对用户程序的接口及其验证抽象起来,使得用户程序的验证无需再关心垃圾收集器的具体实现,并方便用户程序验证和垃圾收集器验证的链接。
最后一部分工作研究了类型安全的垃圾收集过程。给出了一种为基础的类型化汇编语言提供验证的垃圾收集过程的方法,它基于一个开放式的汇编语言级程序逻辑,并使用了第二部分工作的主要思想,将垃圾收集器的细节从类型化汇编语言的类型系统中抽象出去,简化了类型化汇编语言的设计。
同时,本文还讨论了这些工作在计算机辅助定理证明工具COQ中的实现,以及在这些实现中设计和发展的一些提高证明效率的方法和技术。
本文工作的主要贡献和创新包括:1)基于汇编语言层次的一个携带证明程序的验证框架,首次成功地验证了多种垃圾收集算法的汇编级实现代码,以及它们和用户程序的交互过程;2)提出了一种基于抽象数据类型技术的通用方法,能够对垃圾收集器、用户程序以及它们的交互过程进行简洁且严格的验证;3)首次成功地解决了在最小被信任计算基础的前提下为类型化汇编语言提供类型安全的垃圾收集过程这一热点研究问题;4)基于分离逻辑技术,首次成功地从单个内存单元开始构造了标记—清扫式垃圾收集器的具体内存规范。
这些研究工作对减小安全程序设计语言的被信任计算基础进行了有益的尝试——使用形式程序验证技术,携带基础证明的垃圾收集过程就可以被排除出安全程序设计语言的被信任计算基础。同时,它们也为汇编语言级程序的形式验证,特别是为携带证明的代码的技术的应用积累了重要的理论和实践经验。而随着这类技术的进步,更多被信任的软件就可以经过验证而被排除出系统的被信任计算基础。
Safe programming languages such as Java and C# is capable of producing software systems that are free from some pitfalls often seen in software developed with traditional programming languages. However, all the existing safe languages rely on garbage collection mechanism for dynamic memory management. And some of their safety-related features, including the prevention of dangling pointer dereference and memory leak, are provided by garbage collection. Thus, the correctness of the underlying garbage collection is the key to the safety of these languages. Unfortunately, garbage collectors are extremely hard to implement correctly, and their interactions with mutators are often complex and error-prone. For increasing the safety of languages such as Java and C#, it is necessary to rigorously reason about the safety and correctness of garbage collection.
This paper presents the Proof-Carrying Code style formal verification of two garbage collectors against their safety and correctness specifications, as well as the safe interaction between garbage collectors and various mutators, including codes constructed with Typed Assembly Language. The verification work presented is implemented as COQ proofs, and is thus machine-checkable and ready to be distributed in the form of Proof-Carrying Code.
The work presented in this paper includes three major parts. The first part of work verifies two garbage collectors, namely stop-the-world mark-sweep and Yuasa incremental, against their safety and correctness specifications. The specifications, including some intricate invariants like the Weak Tri-color Invariant, are constructed using Separation-Logic style specification language. And the proof is constructed in a Hoare-style program logic.
The second part of work introduces a new uniform approach to verify the safety of the interaction between mutator and garbage collector in Hoare-style program logic. Based on techniques like Abstract Data Type, this approach specifies garbage collector interfaces in an abstract way. Thus the verification of mutator is freed from reason- ing about the details of garbage collector. And the linking of the mutator verification against the verification of garbage collector is easier and more flexible.
The final part of work studies the issue of type-safe garbage collection. It offers an approach of combining Typed Assembly Language with verified garbage collection. Using an open Proof-Carrying Code framework and the ideas in the second part of work, this approach successfully links the code constructed in a Typed Assembly Language with a proved conservative garbage collector, which includes showing that the collector's interface specifications are compatible with the typing rules of the Typed Assembly Language.
Besides, this paper also discusses the COQ implementation issues of the work above, and introduces some ideas and techniques for improving productivity in proof construction.
The work presented in this paper may effectively reduced the Trusted Computing Base of languages like Java and C#, as well as other safe programming systems using garbage collection. And the successful verification of complex garbage collector algorithms is also a valuable experience for Proof-Carrying Code style verification.
本文工作使用基于Hoare逻辑的汇编语言级形式程序验证框架,对垃圾收集器的安全性和正确性,以及垃圾收集器与多种用户程序,特别是类型化汇编语言的交互过程的安全性进行了严格的形式验证。本文工作基于携带证明的代码技术,所有的验证都在计算机辅助定理证明工具COQ中实现为计算机可检查的证明。这样,垃圾收集器和用户程序就能够被构造为一个完整的携带安全性证明的软件包,方便地通过互联网和其他渠道进行发布。
本文的第一部分工作验证了两种典型垃圾收集器的汇编语言实现。该工作使用分离逻辑风格的代码规范语言给出了停止式标记—清扫垃圾收集器和基于初始快照的Yuasa渐进式垃圾收集器的安全规范,并使用Hoare风格的程序逻辑和推理方法证明了垃圾收集器满足其安全规范。
第二部分工作从单独验证垃圾收集器工作存在的不足出发,提出并实现了一种通用的验证垃圾收集器和用户程序交互过程的方法。其核心思想是使用类似抽象数据类型的技术将垃圾收集器对用户程序的接口及其验证抽象起来,使得用户程序的验证无需再关心垃圾收集器的具体实现,并方便用户程序验证和垃圾收集器验证的链接。
最后一部分工作研究了类型安全的垃圾收集过程。给出了一种为基础的类型化汇编语言提供验证的垃圾收集过程的方法,它基于一个开放式的汇编语言级程序逻辑,并使用了第二部分工作的主要思想,将垃圾收集器的细节从类型化汇编语言的类型系统中抽象出去,简化了类型化汇编语言的设计。
同时,本文还讨论了这些工作在计算机辅助定理证明工具COQ中的实现,以及在这些实现中设计和发展的一些提高证明效率的方法和技术。
本文工作的主要贡献和创新包括:1)基于汇编语言层次的一个携带证明程序的验证框架,首次成功地验证了多种垃圾收集算法的汇编级实现代码,以及它们和用户程序的交互过程;2)提出了一种基于抽象数据类型技术的通用方法,能够对垃圾收集器、用户程序以及它们的交互过程进行简洁且严格的验证;3)首次成功地解决了在最小被信任计算基础的前提下为类型化汇编语言提供类型安全的垃圾收集过程这一热点研究问题;4)基于分离逻辑技术,首次成功地从单个内存单元开始构造了标记—清扫式垃圾收集器的具体内存规范。
这些研究工作对减小安全程序设计语言的被信任计算基础进行了有益的尝试——使用形式程序验证技术,携带基础证明的垃圾收集过程就可以被排除出安全程序设计语言的被信任计算基础。同时,它们也为汇编语言级程序的形式验证,特别是为携带证明的代码的技术的应用积累了重要的理论和实践经验。而随着这类技术的进步,更多被信任的软件就可以经过验证而被排除出系统的被信任计算基础。
Safe programming languages such as Java and C# is capable of producing software systems that are free from some pitfalls often seen in software developed with traditional programming languages. However, all the existing safe languages rely on garbage collection mechanism for dynamic memory management. And some of their safety-related features, including the prevention of dangling pointer dereference and memory leak, are provided by garbage collection. Thus, the correctness of the underlying garbage collection is the key to the safety of these languages. Unfortunately, garbage collectors are extremely hard to implement correctly, and their interactions with mutators are often complex and error-prone. For increasing the safety of languages such as Java and C#, it is necessary to rigorously reason about the safety and correctness of garbage collection.
This paper presents the Proof-Carrying Code style formal verification of two garbage collectors against their safety and correctness specifications, as well as the safe interaction between garbage collectors and various mutators, including codes constructed with Typed Assembly Language. The verification work presented is implemented as COQ proofs, and is thus machine-checkable and ready to be distributed in the form of Proof-Carrying Code.
The work presented in this paper includes three major parts. The first part of work verifies two garbage collectors, namely stop-the-world mark-sweep and Yuasa incremental, against their safety and correctness specifications. The specifications, including some intricate invariants like the Weak Tri-color Invariant, are constructed using Separation-Logic style specification language. And the proof is constructed in a Hoare-style program logic.
The second part of work introduces a new uniform approach to verify the safety of the interaction between mutator and garbage collector in Hoare-style program logic. Based on techniques like Abstract Data Type, this approach specifies garbage collector interfaces in an abstract way. Thus the verification of mutator is freed from reason- ing about the details of garbage collector. And the linking of the mutator verification against the verification of garbage collector is easier and more flexible.
The final part of work studies the issue of type-safe garbage collection. It offers an approach of combining Typed Assembly Language with verified garbage collection. Using an open Proof-Carrying Code framework and the ideas in the second part of work, this approach successfully links the code constructed in a Typed Assembly Language with a proved conservative garbage collector, which includes showing that the collector's interface specifications are compatible with the typing rules of the Typed Assembly Language.
Besides, this paper also discusses the COQ implementation issues of the work above, and introduces some ideas and techniques for improving productivity in proof construction.
The work presented in this paper may effectively reduced the Trusted Computing Base of languages like Java and C#, as well as other safe programming systems using garbage collection. And the successful verification of complex garbage collector algorithms is also a valuable experience for Proof-Carrying Code style verification.
引文
AFFELDT R, KOBAYASHI N. 2008. A Coq Library for Verification of Concurrent Programs[J]. Electronic Notes in Theoretical Computer Science, 199:17-32.
APPEL A W. 2001. Foundational Proof-Carrying Code[C]//LICS '01: Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science. Boston, USA: IEEE Computer Society:247-258.
APPEL A W, LEROY X. 2007. A List-machine Benchmark for Mechanized Metatheory[J]. Electronic Notes in Theoretical Computer Science, 174(5):95—108.
AYDEMIR B, BOHANNON A, FAIRBAIRN M, et al. 2005. Mechanized metatheory for the masses: The POPLmark Challenge[EB/OL]. http://alliance.seas.upenn.edu/～plclub/cgi-bin/ poplmark/.
AYDEMIR B, CHARGUERAUD A, PIERCE B C, et al. 2008. Engineering formal metathe-ory[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:3-15.
BAKER H G, JR. 1978. List processing in real time on a serial computer[J]. Communication of ACM, 21(4):280-294.
BARENDREGT H P. 1984. The Lambda Calculus - Its Syntax and Semantics[M]. Amsterdam, Netherlands: North-Holland.
BEN-ARIM. 1984. Algorithms for on-the-fly garbage collection[J]. ACM Transaction on Programming Language System, 6(3): 333-344.
BIRKEDAL L, TORP-SMITH N, REYNOLDS J C. 2004. Local reasoning about a copying garbage collector[C]//POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. New York, NY, USA: ACM Press:220-231.
BOEHM H J, WEISER M. 1988. Garbage Collection in an Uncooperative Environment[J]. Software: Practice and Experience, 18(9):807-820.
BORNAT R, CALCAGNO C, O'HEARN P, et al. 2005. Permission accounting in separation logic[C]//POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 259-270.
BROOKS R A. 1984. Trading data space for reduced time and code space in real-time garbage collection on stock hardware[C]//LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional Programming. New York, NY, USA: ACM Press:256-262.
BURDY L. 2001. B vs. Coq to Prove a Garbage Collector[C]//. BOULTON R J, JACKSON P B. TPHOLs '01: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics. Edinburgh, UK: Springer-Verlag. Lecture Notes on Computer Science.
CAI H, SHAO Z, VAYNBERG A. 2007. Certified self-modifying code[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:66-77.
CALCAGNO C, O'HEARN P, BORNAT R. 2003. Program logic and equivalence in the presence of garbage collection[J]. Electronic Notes in Theoretical Computer Science, 298(3):557—581.
CHANG B Y E, CHLIPALA A J, NECULA G C. 2006. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety[C]//VMCAI '06: Proceedings of 7th International Conference on Verification, Model Checking, and Abstract Interpretation. Charleston, SC, USA,: Springer. Lecture Notes in Computer Science, vol. 3855.
CHEN Y, GE L, HUA B, et al. 2007. Design of a Certifying Compiler Supporting Proof Program Safety[C]//TASE '07: Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering. Shanghai, China: IEEE Computer Society: 117-126.
CHENEY C J. 1970. A nonrecursive list compacting algorithm[J]. Communication of ACM, 13(11):677-678.
CHLIPALA A. 2006. Modular development of certified program verifiers with a proof assis-tant[C]//ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:160-171.
CHLIPALA A. 2007. A certified type-preserving compiler from lambda calculus to assembly language[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:54-65.
CHURCH A. 1936. An unsolvable problem of elementary number theory[J]. American Journal of Mathematics, 58:345-363.
COLLINS G E. 1960. A Method for Overlapping and Erasure of Lists[J]. Communication of ACM, 3(12):655-657.
COQ DEVELOPMENT TEAM. 2007. The Coq Proof Assistant Reference Manual[EB/OL]. http: //coq.inria.fr/.
COQUAND T, HUET G P. 1988. The Calculus of Constructions [J]. Information and Computation, 76(2/3):95-120.
CRARY K. 2003. Toward a Foundational Typed Assembly Language[C]//POPL '03: Proceedings of the 30th ACM Symposium on Principles of Programming Language. New Orleans, LA: ACM Press: 198-212.
CURRY H. 1934. Functionality in Combinatory Logic[J]. Proceedings of the National Academy of Sciences, 20:584-590.
DE BRUIJN N G. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem[J]. Indagationes Mathe-maticae (Proceedings), 75(5):381-392.
DUKSTRA E W, LAMPORT L, MARTIN A J, et al. 1978. On-the-fly garbage collection: an exercise in cooperation[J]. Communication of ACM, 21(11):966—975.
DOLIGEZ D, LEROY X. 1993. A concurrent, generational garbage collector for a multithreaded implementation of ML[C]//POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 113-123.
FENG X, SHAO Z. 2005. Modular verification of concurrent assembly code with dynamic thread creation and termination[C]//ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:254-267.
FENG X, SHAO Z, VAYNBERG A, et al. 2006. Modular Verification of Assembly Code with Stack-Based Control Abstractions[C]//PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming Language Design and Implementation. Ottawa, Canada: ACM Press.
FENG X, FERREIRA R, SHAO Z. 2007a. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning[C]//ESOP '07: Proceedings of 16th European Symposium on Programming.[S.l.]: Springer. Lecture Notes in Computer Science, vol. 4421.
FENG X, NI Z, SHAO Z, et al. 2007b. An Open Framework for Foundational Proof-Carrying Code[C)//TLDI '07: Proceedings of 3rd ACM Workshop on Types in Language Design and Implementation. Nice, France: ACM Press:67-78.
FENG X, SHAO Z, DONG Y, et al. 2008. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads[C]//PLDI '08: Proceedings of 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation. Tucson, Arizona, USA: ACM Press:to appear.
GIRARD J Y. 1987. Linear Logic[J]. Electronic Notes in Theoretical Computer Science, 50:1-102.
GONTHIER G. 1996. Verifying the Safety of a Practical Concurrent Garbage Collector[C]//. ALUR R, HENZINGER T. CAV '96: Proceedings of 8th International Conference on Computer Aided Verification. New Brunswick, NJ: Springer-Verlag. Lecture Notes in Computer Science.
GOSLING J, JOY B, STEELE G, et al. 2000. Java Language Specification, Second Edition: The Java Series[M]. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc.
GRIES D. 1977. An exercise in proving parallel programs correct[J]. Communication of ACM, 20(12):921-930.
GRIES D. 1978. Corrigendum[J]. Communication of ACM, 21(12): 1048.
GUO Y, JIANG X, CHEN Y, et al. 2007. A Certified Thread Library for Multithreaded User Pro-grams[C]//TASE '07: Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering. Shanghai, China: IEEE Computer Society: 127-136.
GUY L. STEELE J. 1975. Multiprocessing compactifying garbage collection[J]. Communication of ACM, 18(9):495-508.
HAMID N A, SHAO Z, TRIFONOV V, et al. 2002. A Syntactic Approach to Foundational Proof-Carrying Code[C]//LICS '02: Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science. Copenhagen, Denmark: IEEE CS:89-100.
HART T P, EVANS T G. 1964. Notes on Implementing LISP for the M-460 Computer[C]//The Programming Language LISP: Its Operation and Applications. Cambridge, Mass.: Information International: 191-203.
HAWBLITZEL C, HUANG H, WITTIE L, et al. 2007. A Garbage-Collecting Typed Assembly Language[C]//TLDI '07: Proceedings of 3rd ACM SIGPLAN International Workshop on Types in Language Design and Implementation. Nice, France: ACM Press.
HEJLSBERG A, WILTAMUTH S, GOLDE P. 2006. C# Programming Language, The (2nd Edition) (Microsoft .NET Development Series)[M]. Boston, MA: Addison-Wesley Professional.
HOARE C A R. 1969. An axiomatic basis for computer programming[J]. Communication of ACM, 12(10):576-580.
HOWARD W A. 1980. The Formulae-as-types Notion of Construction[M]//. SELDIN J P, HIND-LEY J R. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. London: Academic Press:479-490.
HUDSON R L, MOSS J E B. 2001. Sapphire: copying GC without stopping the world[C]//JGI '01: Proceedings of the 2001 joint ACM-ISCOPE conference on Java Grande. New York, NY, USA: ACM:48-57.
HUNT G C, LARUS J R. 2007. Singularity: rethinking the software stack[J]. SIGOPS Operating System Review, 41(2):37-49.
HUNTER R, KRISHNAMURTHI S. 2003. A model of garbage collection for OO lan-guages[C]//FOOL 10: Proceedings of the 10th International Workshop on Foundations of Object-Oriented Language. New York, NY, USA: ACM Press.
ISHTIAQ S S, O'HEARN P W. 2001. BI as an assertion language for mutable data structures [C]//POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 14-26.
JACKSON P. 1998. Verifying a Garbage Collection Algorithm[C]//TPHOLs '98: Proceedings of 11th International Conference on Theorem Proving in Higher Order Logics. Canberra: Springer-Verlag. Lecture Notes in Computer Science, vol. 1479.
JONES R E. 1996. Garbage Collection: Algorithms for Automatic Dynamic Memory Manage-ment[M]. New York, USA: Wiley: 403.
KUNG H T, SONG S W. 1977. An Efficient Parallel Garbage Collection System and its Correctness Proof[C]//Proceedings of IEEE Symposium on Foundations of Computer Science.fS.l.]: IEEE Computer Society: 120-131.
LARUS J. 2007. SPIM: a MIPS32 Simulator[EB/OL], http://www.cs.wisc.edu/～larus/spim.html.
LEAGUE C, TRIFONOV V, SHAO Z. 2001. Type-Preserving Compilation of Featherweight Java[C]//FOOL 8: Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages. New York, NY, USA: ACM Press.
LEE S, DE ROEVER W P, GERHART S. 1979. The Evolution of List Copying Algorithms[C]//POPL '79: Proceedings of 6th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. San Antonio, Texas: ACM Press:53-56.
LEROY X. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant[C]//POPL '06: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:42-54.
LEROY X, DOLIGEZ D, GARRIGUE J, et al. 2007. The Objective Caml system release 3.10[EB/OL]. http://caml.inria.fr/.
LIN C, MCCREIGHT A, SHAO Z, et al. 2007a. Foundational Typed Assembly Language with Certified Garbage Collection[C]//TASE '07: Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering. Shanghai, China: IEEE Computer Society:326-335, http://flint.cs.yale.edu/flint/publications/talgc.html.
LIN C, CHEN Y, LI L, et al. 2007b. Garbage Collector Verification for Proof-Carrying Code[J]. Journal of Computer Science and Technology, 22(3):426-437. http://ssg.ustcsz.edu.cn/～cxlin/ gcpaper/.
LIN C, CHEN Y, HUA B. 2007c. Verification of a real-time garbage collector in Hoare-style logic[R]. Hefei, China: University of Science and Technology of China, http://ssg.ustcsz.edu. cn/～cxlin/yuasa/.
LISKOV B, ZILLES S. 1974. Programming with abstract data types[C]//Proceedings of the ACM SIGPLAN symposium on Very high level languages. New York, NY, USA: ACM:50-59.
MARTI N, AFFELDT R, YONEZAWA A. 2006. Formal Verification of the Heap Manager of an Operating System Using Separation Logic[C]//ICFEM '06: Proceedings of the 8th Interna- tional Conference on Formal Engineering Methods. Utrecht, The Netherlands: Springer. Lecture Notes in Computer Science, vol. 4260.
MCCARTHY J. 1960. Recursive Functions of Symbolic Expressions and their Computation by Machine[J]. Communication of ACM, 3:184-195.
MCCARTHY J. 1978. History of LISP[C]//. WEXELBLAT R L. HOPL I: Proceedings of the 1st ACM SIGPLAN Conference on History of Programming Languages. New York, US: Academic Press: 173-197.
MCCREIGHT A, SHAO Z, LIN C, et al. 2007. A General Framework for Certifying Garbage Collectors and Their Mutators[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming Language Design and Implementation. San Diego, CA, USA: ACM Press:468-479, http://flint.cs.yale.edu/flint/publications/hgc.html.
MCGACHEY P, ADL-TABATABAI A R, HUDSON R L, et al. 2008. Concurrent GC leveraging transactional memory[C]//PPoPP '08: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming. New York, NY, USA: ACM:217-226.
MICROSOFT CORPORATION. 2007. The F# Programming Language[EB/OL]. http://research. microsoft.com/fsharp/.
MILNER R, TOFTE M, HARPER R, et al. 1997. The Definition of Standard ML (Revised)[M]. Cambridge, MA: MIT Press.
MINSKY M L. 1963. A Lisp Garbage Collector Algorithm Using Serial Secondary Storage[R]. MIT, Cambridge, MA: Project MAC.
MIPS TECHNOLOGIES. 2005. MIPS32? Architecture For Programmers Volume II: Instruction Set, v2.50[EB].
MONNIER S, SAHA B, SHAO Z. 2001. Principled Scavenging[C]//PLDI '01: Proceedings of 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, US: ACM Press:81-91.
MORRISETT G, WALKER D, CRARY K, et al. 1999a. From system F to typed assembly language[J]. ACM Transaction on Programming Language and System, 21(3):527-568.
MORRISETT G, CRARY K, GLEW N, et al. 1999b. TALx86: A Realistic Typed Assembly Language[C]//Proceedings of the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software. Atlanta, GA, USA: ACM Press:25-35.
MOZILLA FOUNDATION. 2007. Mozilla Foundation Security Advisories[EB/OL]. http://www.mozilla.org/security/announce/.
NECULA G C. 1997. Proof-Carrying Code[C]//POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges. Paris: ACM Press: 106-119.
NI Z, SHAO Z. 2006. Certified Assembly Programming with Embedded Code Pointers[C]//POPL '06: Proceedings of 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. Charleston, South Carolina: ACM Press.
NIETO L P, ESPARZA J. 2000. Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL[C]//MFCS '00: Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science. London, UK: Springer-Verlag:619-628.
NIST. 2006. Vulnerability Summary [EB/OL]. http://nvd.nist.gov/nvd.cfm?cvename= CVE-2006-3451.
OHEARN P W. 2007. Resources, concurrency, and local reasoning[J]. Electronic Notes in Theoretical Computer Science, 375(1-3):271-307.
O'HEARN P W, REYNOLDS J C, YANG H. 2001. Local Reasoning about Programs that Alter Data Structures[C]//CSL '01: Proceedings of the 15th International Workshop on Computer Science Logic. London, UK: Springer-Verlag:1-19.
O'HEARN P W, YANG H, REYNOLDS J C. 2004. Separation and information hiding[C]//POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:268-280.
PARKINSON M J, BIERMAN G M. 2008. Separation logic, abstraction and inheritance[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:75-86.
PAUL W, BROY M, IN DER RIEDEN T. 2007. The Verisoft Project[EB/OL]. http://www.verisoft. de/.
PAULIN-MOHRING C. 1993. Inductive definitions in the system Coq—rules and proper-ties[C]//TLCA '93: Proceedings of 5th International Conference on Typed Lambda Calculi and Applications. Utrecht, The Netherlands: Springer-Verlag. Lecture Notes in Computer Science, vol. 664.
PIRINEN P P. 1998. Barrier techniques for incremental tracing[C]//ISMM '98: Proceedings of the 1st international symposium on Memory management. New York, NY, USA: ACM Press:20-25.
REYNOLDS J C. 2002. Separation Logic: A Logic for Shared Mutable Data Structures[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:55-74.
RUSSINOFF D M. 1994. A Mechanically Verified Incremental Garbage ColIector[J]. Formal Aspects of Computing, 6:359-390.
SCHORR H, WAITE W. 1967. An Efficient Machine Independent Procedure for Garbage Collection in Various List Structures[J]. Communication of ACM, 10(8):501-506.
TRISTAN J B, LEROY X. 2008. Formal verification of translation validators: a case study on instruction scheduling optimizations[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 17-27.
VAFEIADIS V, PARKINSON M J. 2007. A Marriage of Rely/Guarantee and Separation Logic[C]//CONCUR '07: Proceedings of 18th International Conference on Concurrency Theory. Lisbon, Portugal: Springer. Lecture Notes in Computer Science, vol. 4703.
VANDERWAART J C, CRARY K. 2003. A typed interface for garbage collection[C]//TLDI '03: Proceedings of 1st ACM SIGPLAN International Workshop on Types in Language Design and Implementation. New York, NY, USA: ACM Press: 109-122.
VECHEV M T, YAHAV E, BACON D F. 2006. Correctness-preserving derivation of concurrent garbage collection algorithms[C]//PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming Language Design and Implementation. New York, NY, USA: ACM Press:341-353.
VECHEV M T, YAHAV E, BACON D F, et al. 2007. CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:456-467.
WANG D C, APPEL A W. 2001. Type-preserving garbage collectors[C]//POPL '01: Proceedings of 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. London, United Kingdom: ACM Press: 166-178.
WILSON P R. 1992. Uniprocessor Garbage Collection Techniques[C]//IWMM '92: Proceedings of the 1992 International Workshop on Memory Management. Saint-Malo (France): Springer-Verlag.
WRIGHT A K, FELLEISEN M. 1994. A syntactic approach to type soundness[J]. Information and Computation, 115(1):38-94.
YELOWITZ L, DUNCAN A G. 1977. Abstractions, Instantiations and Proofs of Marking Algorithms[J]. SIGPLAN Notice, 12(8): 13-21.
YU D, SHAO Z. 2004. Verification of safety properties for concurrent assembly code[C]//ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM: 175-188.
YU D, HAMID N A, SHAO Z. 2004. Building Certified Libraries for PCC: Dynamic Storage Allocation[J]. Science of Computer Programming, 50(1-3): 101—127.
YUASA T. 1990. Real-time garbage collection on general-purpose machines[J]. Journal of Systems and Software, 11(3):181-198.
APPEL A W. 2001. Foundational Proof-Carrying Code[C]//LICS '01: Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science. Boston, USA: IEEE Computer Society:247-258.
APPEL A W, LEROY X. 2007. A List-machine Benchmark for Mechanized Metatheory[J]. Electronic Notes in Theoretical Computer Science, 174(5):95—108.
AYDEMIR B, BOHANNON A, FAIRBAIRN M, et al. 2005. Mechanized metatheory for the masses: The POPLmark Challenge[EB/OL]. http://alliance.seas.upenn.edu/～plclub/cgi-bin/ poplmark/.
AYDEMIR B, CHARGUERAUD A, PIERCE B C, et al. 2008. Engineering formal metathe-ory[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:3-15.
BAKER H G, JR. 1978. List processing in real time on a serial computer[J]. Communication of ACM, 21(4):280-294.
BARENDREGT H P. 1984. The Lambda Calculus - Its Syntax and Semantics[M]. Amsterdam, Netherlands: North-Holland.
BEN-ARIM. 1984. Algorithms for on-the-fly garbage collection[J]. ACM Transaction on Programming Language System, 6(3): 333-344.
BIRKEDAL L, TORP-SMITH N, REYNOLDS J C. 2004. Local reasoning about a copying garbage collector[C]//POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. New York, NY, USA: ACM Press:220-231.
BOEHM H J, WEISER M. 1988. Garbage Collection in an Uncooperative Environment[J]. Software: Practice and Experience, 18(9):807-820.
BORNAT R, CALCAGNO C, O'HEARN P, et al. 2005. Permission accounting in separation logic[C]//POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 259-270.
BROOKS R A. 1984. Trading data space for reduced time and code space in real-time garbage collection on stock hardware[C]//LFP '84: Proceedings of the 1984 ACM Symposium on LISP and functional Programming. New York, NY, USA: ACM Press:256-262.
BURDY L. 2001. B vs. Coq to Prove a Garbage Collector[C]//. BOULTON R J, JACKSON P B. TPHOLs '01: Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics. Edinburgh, UK: Springer-Verlag. Lecture Notes on Computer Science.
CAI H, SHAO Z, VAYNBERG A. 2007. Certified self-modifying code[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:66-77.
CALCAGNO C, O'HEARN P, BORNAT R. 2003. Program logic and equivalence in the presence of garbage collection[J]. Electronic Notes in Theoretical Computer Science, 298(3):557—581.
CHANG B Y E, CHLIPALA A J, NECULA G C. 2006. A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety[C]//VMCAI '06: Proceedings of 7th International Conference on Verification, Model Checking, and Abstract Interpretation. Charleston, SC, USA,: Springer. Lecture Notes in Computer Science, vol. 3855.
CHEN Y, GE L, HUA B, et al. 2007. Design of a Certifying Compiler Supporting Proof Program Safety[C]//TASE '07: Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering. Shanghai, China: IEEE Computer Society: 117-126.
CHENEY C J. 1970. A nonrecursive list compacting algorithm[J]. Communication of ACM, 13(11):677-678.
CHLIPALA A. 2006. Modular development of certified program verifiers with a proof assis-tant[C]//ICFP '06: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:160-171.
CHLIPALA A. 2007. A certified type-preserving compiler from lambda calculus to assembly language[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:54-65.
CHURCH A. 1936. An unsolvable problem of elementary number theory[J]. American Journal of Mathematics, 58:345-363.
COLLINS G E. 1960. A Method for Overlapping and Erasure of Lists[J]. Communication of ACM, 3(12):655-657.
COQ DEVELOPMENT TEAM. 2007. The Coq Proof Assistant Reference Manual[EB/OL]. http: //coq.inria.fr/.
COQUAND T, HUET G P. 1988. The Calculus of Constructions [J]. Information and Computation, 76(2/3):95-120.
CRARY K. 2003. Toward a Foundational Typed Assembly Language[C]//POPL '03: Proceedings of the 30th ACM Symposium on Principles of Programming Language. New Orleans, LA: ACM Press: 198-212.
CURRY H. 1934. Functionality in Combinatory Logic[J]. Proceedings of the National Academy of Sciences, 20:584-590.
DE BRUIJN N G. 1972. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem[J]. Indagationes Mathe-maticae (Proceedings), 75(5):381-392.
DUKSTRA E W, LAMPORT L, MARTIN A J, et al. 1978. On-the-fly garbage collection: an exercise in cooperation[J]. Communication of ACM, 21(11):966—975.
DOLIGEZ D, LEROY X. 1993. A concurrent, generational garbage collector for a multithreaded implementation of ML[C]//POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 113-123.
FENG X, SHAO Z. 2005. Modular verification of concurrent assembly code with dynamic thread creation and termination[C]//ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM:254-267.
FENG X, SHAO Z, VAYNBERG A, et al. 2006. Modular Verification of Assembly Code with Stack-Based Control Abstractions[C]//PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming Language Design and Implementation. Ottawa, Canada: ACM Press.
FENG X, FERREIRA R, SHAO Z. 2007a. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning[C]//ESOP '07: Proceedings of 16th European Symposium on Programming.[S.l.]: Springer. Lecture Notes in Computer Science, vol. 4421.
FENG X, NI Z, SHAO Z, et al. 2007b. An Open Framework for Foundational Proof-Carrying Code[C)//TLDI '07: Proceedings of 3rd ACM Workshop on Types in Language Design and Implementation. Nice, France: ACM Press:67-78.
FENG X, SHAO Z, DONG Y, et al. 2008. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads[C]//PLDI '08: Proceedings of 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation. Tucson, Arizona, USA: ACM Press:to appear.
GIRARD J Y. 1987. Linear Logic[J]. Electronic Notes in Theoretical Computer Science, 50:1-102.
GONTHIER G. 1996. Verifying the Safety of a Practical Concurrent Garbage Collector[C]//. ALUR R, HENZINGER T. CAV '96: Proceedings of 8th International Conference on Computer Aided Verification. New Brunswick, NJ: Springer-Verlag. Lecture Notes in Computer Science.
GOSLING J, JOY B, STEELE G, et al. 2000. Java Language Specification, Second Edition: The Java Series[M]. Boston, MA, USA: Addison-Wesley Longman Publishing Co., Inc.
GRIES D. 1977. An exercise in proving parallel programs correct[J]. Communication of ACM, 20(12):921-930.
GRIES D. 1978. Corrigendum[J]. Communication of ACM, 21(12): 1048.
GUO Y, JIANG X, CHEN Y, et al. 2007. A Certified Thread Library for Multithreaded User Pro-grams[C]//TASE '07: Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering. Shanghai, China: IEEE Computer Society: 127-136.
GUY L. STEELE J. 1975. Multiprocessing compactifying garbage collection[J]. Communication of ACM, 18(9):495-508.
HAMID N A, SHAO Z, TRIFONOV V, et al. 2002. A Syntactic Approach to Foundational Proof-Carrying Code[C]//LICS '02: Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science. Copenhagen, Denmark: IEEE CS:89-100.
HART T P, EVANS T G. 1964. Notes on Implementing LISP for the M-460 Computer[C]//The Programming Language LISP: Its Operation and Applications. Cambridge, Mass.: Information International: 191-203.
HAWBLITZEL C, HUANG H, WITTIE L, et al. 2007. A Garbage-Collecting Typed Assembly Language[C]//TLDI '07: Proceedings of 3rd ACM SIGPLAN International Workshop on Types in Language Design and Implementation. Nice, France: ACM Press.
HEJLSBERG A, WILTAMUTH S, GOLDE P. 2006. C# Programming Language, The (2nd Edition) (Microsoft .NET Development Series)[M]. Boston, MA: Addison-Wesley Professional.
HOARE C A R. 1969. An axiomatic basis for computer programming[J]. Communication of ACM, 12(10):576-580.
HOWARD W A. 1980. The Formulae-as-types Notion of Construction[M]//. SELDIN J P, HIND-LEY J R. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. London: Academic Press:479-490.
HUDSON R L, MOSS J E B. 2001. Sapphire: copying GC without stopping the world[C]//JGI '01: Proceedings of the 2001 joint ACM-ISCOPE conference on Java Grande. New York, NY, USA: ACM:48-57.
HUNT G C, LARUS J R. 2007. Singularity: rethinking the software stack[J]. SIGOPS Operating System Review, 41(2):37-49.
HUNTER R, KRISHNAMURTHI S. 2003. A model of garbage collection for OO lan-guages[C]//FOOL 10: Proceedings of the 10th International Workshop on Foundations of Object-Oriented Language. New York, NY, USA: ACM Press.
ISHTIAQ S S, O'HEARN P W. 2001. BI as an assertion language for mutable data structures [C]//POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 14-26.
JACKSON P. 1998. Verifying a Garbage Collection Algorithm[C]//TPHOLs '98: Proceedings of 11th International Conference on Theorem Proving in Higher Order Logics. Canberra: Springer-Verlag. Lecture Notes in Computer Science, vol. 1479.
JONES R E. 1996. Garbage Collection: Algorithms for Automatic Dynamic Memory Manage-ment[M]. New York, USA: Wiley: 403.
KUNG H T, SONG S W. 1977. An Efficient Parallel Garbage Collection System and its Correctness Proof[C]//Proceedings of IEEE Symposium on Foundations of Computer Science.fS.l.]: IEEE Computer Society: 120-131.
LARUS J. 2007. SPIM: a MIPS32 Simulator[EB/OL], http://www.cs.wisc.edu/～larus/spim.html.
LEAGUE C, TRIFONOV V, SHAO Z. 2001. Type-Preserving Compilation of Featherweight Java[C]//FOOL 8: Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages. New York, NY, USA: ACM Press.
LEE S, DE ROEVER W P, GERHART S. 1979. The Evolution of List Copying Algorithms[C]//POPL '79: Proceedings of 6th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. San Antonio, Texas: ACM Press:53-56.
LEROY X. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant[C]//POPL '06: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:42-54.
LEROY X, DOLIGEZ D, GARRIGUE J, et al. 2007. The Objective Caml system release 3.10[EB/OL]. http://caml.inria.fr/.
LIN C, MCCREIGHT A, SHAO Z, et al. 2007a. Foundational Typed Assembly Language with Certified Garbage Collection[C]//TASE '07: Proceedings of 1st IEEE IFIP International Symposium on Theoretical Aspects of Software Engineering. Shanghai, China: IEEE Computer Society:326-335, http://flint.cs.yale.edu/flint/publications/talgc.html.
LIN C, CHEN Y, LI L, et al. 2007b. Garbage Collector Verification for Proof-Carrying Code[J]. Journal of Computer Science and Technology, 22(3):426-437. http://ssg.ustcsz.edu.cn/～cxlin/ gcpaper/.
LIN C, CHEN Y, HUA B. 2007c. Verification of a real-time garbage collector in Hoare-style logic[R]. Hefei, China: University of Science and Technology of China, http://ssg.ustcsz.edu. cn/～cxlin/yuasa/.
LISKOV B, ZILLES S. 1974. Programming with abstract data types[C]//Proceedings of the ACM SIGPLAN symposium on Very high level languages. New York, NY, USA: ACM:50-59.
MARTI N, AFFELDT R, YONEZAWA A. 2006. Formal Verification of the Heap Manager of an Operating System Using Separation Logic[C]//ICFEM '06: Proceedings of the 8th Interna- tional Conference on Formal Engineering Methods. Utrecht, The Netherlands: Springer. Lecture Notes in Computer Science, vol. 4260.
MCCARTHY J. 1960. Recursive Functions of Symbolic Expressions and their Computation by Machine[J]. Communication of ACM, 3:184-195.
MCCARTHY J. 1978. History of LISP[C]//. WEXELBLAT R L. HOPL I: Proceedings of the 1st ACM SIGPLAN Conference on History of Programming Languages. New York, US: Academic Press: 173-197.
MCCREIGHT A, SHAO Z, LIN C, et al. 2007. A General Framework for Certifying Garbage Collectors and Their Mutators[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming Language Design and Implementation. San Diego, CA, USA: ACM Press:468-479, http://flint.cs.yale.edu/flint/publications/hgc.html.
MCGACHEY P, ADL-TABATABAI A R, HUDSON R L, et al. 2008. Concurrent GC leveraging transactional memory[C]//PPoPP '08: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming. New York, NY, USA: ACM:217-226.
MICROSOFT CORPORATION. 2007. The F# Programming Language[EB/OL]. http://research. microsoft.com/fsharp/.
MILNER R, TOFTE M, HARPER R, et al. 1997. The Definition of Standard ML (Revised)[M]. Cambridge, MA: MIT Press.
MINSKY M L. 1963. A Lisp Garbage Collector Algorithm Using Serial Secondary Storage[R]. MIT, Cambridge, MA: Project MAC.
MIPS TECHNOLOGIES. 2005. MIPS32? Architecture For Programmers Volume II: Instruction Set, v2.50[EB].
MONNIER S, SAHA B, SHAO Z. 2001. Principled Scavenging[C]//PLDI '01: Proceedings of 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation. New York, US: ACM Press:81-91.
MORRISETT G, WALKER D, CRARY K, et al. 1999a. From system F to typed assembly language[J]. ACM Transaction on Programming Language and System, 21(3):527-568.
MORRISETT G, CRARY K, GLEW N, et al. 1999b. TALx86: A Realistic Typed Assembly Language[C]//Proceedings of the 1999 ACM SIGPLAN Workshop on Compiler Support for System Software. Atlanta, GA, USA: ACM Press:25-35.
MOZILLA FOUNDATION. 2007. Mozilla Foundation Security Advisories[EB/OL]. http://www.mozilla.org/security/announce/.
NECULA G C. 1997. Proof-Carrying Code[C]//POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges. Paris: ACM Press: 106-119.
NI Z, SHAO Z. 2006. Certified Assembly Programming with Embedded Code Pointers[C]//POPL '06: Proceedings of 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. Charleston, South Carolina: ACM Press.
NIETO L P, ESPARZA J. 2000. Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL[C]//MFCS '00: Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science. London, UK: Springer-Verlag:619-628.
NIST. 2006. Vulnerability Summary [EB/OL]. http://nvd.nist.gov/nvd.cfm?cvename= CVE-2006-3451.
OHEARN P W. 2007. Resources, concurrency, and local reasoning[J]. Electronic Notes in Theoretical Computer Science, 375(1-3):271-307.
O'HEARN P W, REYNOLDS J C, YANG H. 2001. Local Reasoning about Programs that Alter Data Structures[C]//CSL '01: Proceedings of the 15th International Workshop on Computer Science Logic. London, UK: Springer-Verlag:1-19.
O'HEARN P W, YANG H, REYNOLDS J C. 2004. Separation and information hiding[C]//POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM Press:268-280.
PARKINSON M J, BIERMAN G M. 2008. Separation logic, abstraction and inheritance[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM:75-86.
PAUL W, BROY M, IN DER RIEDEN T. 2007. The Verisoft Project[EB/OL]. http://www.verisoft. de/.
PAULIN-MOHRING C. 1993. Inductive definitions in the system Coq—rules and proper-ties[C]//TLCA '93: Proceedings of 5th International Conference on Typed Lambda Calculi and Applications. Utrecht, The Netherlands: Springer-Verlag. Lecture Notes in Computer Science, vol. 664.
PIRINEN P P. 1998. Barrier techniques for incremental tracing[C]//ISMM '98: Proceedings of the 1st international symposium on Memory management. New York, NY, USA: ACM Press:20-25.
REYNOLDS J C. 2002. Separation Logic: A Logic for Shared Mutable Data Structures[C]//LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. Washington, DC, USA: IEEE Computer Society:55-74.
RUSSINOFF D M. 1994. A Mechanically Verified Incremental Garbage ColIector[J]. Formal Aspects of Computing, 6:359-390.
SCHORR H, WAITE W. 1967. An Efficient Machine Independent Procedure for Garbage Collection in Various List Structures[J]. Communication of ACM, 10(8):501-506.
TRISTAN J B, LEROY X. 2008. Formal verification of translation validators: a case study on instruction scheduling optimizations[C]//POPL '08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, NY, USA: ACM: 17-27.
VAFEIADIS V, PARKINSON M J. 2007. A Marriage of Rely/Guarantee and Separation Logic[C]//CONCUR '07: Proceedings of 18th International Conference on Concurrency Theory. Lisbon, Portugal: Springer. Lecture Notes in Computer Science, vol. 4703.
VANDERWAART J C, CRARY K. 2003. A typed interface for garbage collection[C]//TLDI '03: Proceedings of 1st ACM SIGPLAN International Workshop on Types in Language Design and Implementation. New York, NY, USA: ACM Press: 109-122.
VECHEV M T, YAHAV E, BACON D F. 2006. Correctness-preserving derivation of concurrent garbage collection algorithms[C]//PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming Language Design and Implementation. New York, NY, USA: ACM Press:341-353.
VECHEV M T, YAHAV E, BACON D F, et al. 2007. CGCExplorer: a semi-automated search procedure for provably correct concurrent collectors[C]//PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. New York, NY, USA: ACM:456-467.
WANG D C, APPEL A W. 2001. Type-preserving garbage collectors[C]//POPL '01: Proceedings of 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language. London, United Kingdom: ACM Press: 166-178.
WILSON P R. 1992. Uniprocessor Garbage Collection Techniques[C]//IWMM '92: Proceedings of the 1992 International Workshop on Memory Management. Saint-Malo (France): Springer-Verlag.
WRIGHT A K, FELLEISEN M. 1994. A syntactic approach to type soundness[J]. Information and Computation, 115(1):38-94.
YELOWITZ L, DUNCAN A G. 1977. Abstractions, Instantiations and Proofs of Marking Algorithms[J]. SIGPLAN Notice, 12(8): 13-21.
YU D, SHAO Z. 2004. Verification of safety properties for concurrent assembly code[C]//ICFP '04: Proceedings of the ninth ACM SIGPLAN international conference on Functional programming. New York, NY, USA: ACM: 175-188.
YU D, HAMID N A, SHAO Z. 2004. Building Certified Libraries for PCC: Dynamic Storage Allocation[J]. Science of Computer Programming, 50(1-3): 101—127.
YUASA T. 1990. Real-time garbage collection on general-purpose machines[J]. Journal of Systems and Software, 11(3):181-198.