| Abstract | 第6页 |
| Résumé | 第7-8页 |
| Acknowledgements | 第8-13页 |
| 1 Introduction | 第13-19页 |
| 1.1 Motivation | 第14-16页 |
| 1.2 Contributions | 第16-18页 |
| 1.3 Organisation | 第18-19页 |
| I FORMALIZATION OF SEQUENTIAL DYNAMIC MEMORYALLOCATORS | 第19-78页 |
| 2 Sequential Dynamic Memory Allocators | 第20-35页 |
| 2.1 Basic Elements of SDMA | 第21-25页 |
| 2.1.1 Memory Structure | 第21页 |
| 2.1.2 Interface for Clients | 第21-22页 |
| 2.1.3 Interface Implementation | 第22-25页 |
| 2.2 Taxonomy of SDMA | 第25-29页 |
| 2.2.1 Heap List | 第25-26页 |
| 2.2.2 Fragmentation | 第26-28页 |
| 2.2.3 Free List | 第28-29页 |
| 2.3 Case Studies | 第29-33页 |
| 2.3.1 Collected SDMA | 第30-33页 |
| 2.3.2 Related Work | 第33页 |
| 2.4 Challenges for Formalization | 第33-35页 |
| 3 Formalization Strategy | 第35-54页 |
| 3.1 Preliminaries | 第36-45页 |
| 3.1.1 State Machine | 第36-41页 |
| 3.1.2 Refinement | 第41-45页 |
| 3.2 Abstract Specification for SDMA | 第45-49页 |
| 3.2.1 Formalization Hypotheses | 第46页 |
| 3.2.2 State | 第46-48页 |
| 3.2.3 Invariants | 第48页 |
| 3.2.4 Transition Rules | 第48-49页 |
| 3.3 Refinement Strategy for SDMA | 第49-54页 |
| 3.3.1 Refinement Steps | 第50-51页 |
| 3.3.2 Refinement Principles | 第51-54页 |
| 4 Refinement-based Formalization | 第54-78页 |
| 4.1 Heap List Modelling | 第54-66页 |
| 4.1.1 State and Invariants | 第55-57页 |
| 4.1.2 Basic Heap List Operations | 第57-60页 |
| 4.1.3 Models for Heap List SDMA | 第60-66页 |
| 4.2 Free List Modelling | 第66-75页 |
| 4.2.1 States and Invariants | 第66-69页 |
| 4.2.2 Basic Free List Operations | 第69-71页 |
| 4.2.3 Models for Free List SDMA | 第71-75页 |
| 4.3 Applications of Formal Models | 第75-77页 |
| 4.4 Related Work and Conclusion | 第77-78页 |
| II Static Analysis of Sequential Dynamic Memory Allocators | 第78-163页 |
| 5 Separation Logic Fragment for SDMA | 第79-94页 |
| 5.1 Preliminaries | 第80-83页 |
| 5.1.1 Hoare Logic | 第80页 |
| 5.1.2 Symbolic Heap Fragment of Separation Logic | 第80-83页 |
| 5.2 Separation Logic for Memory Allocators | 第83-87页 |
| 5.2.1 Syntax of SLMA | 第83-87页 |
| 5.2.2 Semantics of SLMA | 第87页 |
| 5.3 Properties | 第87-94页 |
| 5.3.1 Expressiveness | 第89页 |
| 5.3.2 Transformation Rules | 第89-90页 |
| 5.3.3 Satisfiability | 第90-92页 |
| 5.3.4 Entailment Checking | 第92-94页 |
| 6 Logic-based Abstract Domain | 第94-126页 |
| 6.1 Abstract Interpretation Preliminaries | 第95-104页 |
| 6.1.1 A Simple Imperative Language | 第95-97页 |
| 6.1.2 Abstract Interpretation | 第97-102页 |
| 6.1.3 Existing Abstract Domains | 第102-104页 |
| 6.2 Programming Language | 第104-110页 |
| 6.2.1 Programming language syntax | 第104-105页 |
| 6.2.2 Concrete Memory States | 第105-106页 |
| 6.2.3 Concrete Program Semantics | 第106-110页 |
| 6.3 Abstract Domain Based on SLMA | 第110-126页 |
| 6.3.1 Numerical Abstract Domain | 第110-111页 |
| 6.3.2 Data Words Domain | 第111-114页 |
| 6.3.3 Shape Abstract Domain | 第114-117页 |
| 6.3.4 Shape-Value Domain | 第117-119页 |
| 6.3.5 Extended Symbolic Heap Domain | 第119-121页 |
| 6.3.6 Abstract Value | 第121-122页 |
| 6.3.7 Lattice Operators | 第122-126页 |
| 7 Static Analysis Operations and Algorithm | 第126-160页 |
| 7.1 Abstract Postcondition | 第126-128页 |
| 7.2 Hierarchical Unfolding and Folding | 第128-144页 |
| 7.2.1 Abstract Operations in Shape Domain G] | 第128-133页 |
| 7.2.2 Abstract Operations in Data Words Domain W] | 第133-135页 |
| 7.2.3 Abstract Operations in Shape-value Domain H] | 第135-139页 |
| 7.2.4 Hierarchical Unfolding | 第139-142页 |
| 7.2.5 Hierarchical Folding | 第142-144页 |
| 7.3 Abstract Transformers | 第144-155页 |
| 7.3.1 Assignments | 第146-153页 |
| 7.3.2 Condition Tests | 第153-155页 |
| 7.4 Analysis Algorithm | 第155-158页 |
| 7.4.1 Main principles | 第155-157页 |
| 7.4.2 Experiments | 第157-158页 |
| 7.5 Related Work and Conclusion | 第158-160页 |
| 8 Conclusion | 第160-163页 |
| 8.1 Summary | 第160-161页 |
| 8.2 Discussion | 第161-162页 |
| 8.3 Future Work | 第162-163页 |
| List of Figures | 第163-165页 |
| List of Tables | 第165-167页 |
| List of Symbols | 第167-170页 |
| Bibliography | 第170-181页 |
