\BOOKMARK [0][-]{chapter.0}{Table of Contents}{}% 1
\BOOKMARK [0][-]{chapter*.4}{List of Tables}{}% 2
\BOOKMARK [0][-]{chapter*.5}{List of Figures}{}% 3
\BOOKMARK [0][-]{chapter*.6}{Abstract}{}% 4
\BOOKMARK [-1][-]{part.1}{Part I \040Preliminaries}{}% 5
\BOOKMARK [0][-]{chapter.1}{1 Introduction}{part.1}% 6
\BOOKMARK [1][-]{section.1.1}{1.1 Motivation}{chapter.1}% 7
\BOOKMARK [1][-]{section.1.2}{1.2 Contributions}{chapter.1}% 8
\BOOKMARK [2][-]{subsection.1.2.1}{1.2.1 A contract theory for message-passing programs}{section.1.2}% 9
\BOOKMARK [2][-]{subsection.1.2.2}{1.2.2 A method for verifying collective contracts}{section.1.2}% 10
\BOOKMARK [2][-]{subsection.1.2.3}{1.2.3 An MPI Specification Language}{section.1.2}% 11
\BOOKMARK [2][-]{subsection.1.2.4}{1.2.4 A Prototype MPI Contract-Based Verification Tool}{section.1.2}% 12
\BOOKMARK [1][-]{section.1.3}{1.3 Outline}{chapter.1}% 13
\BOOKMARK [0][-]{chapter.2}{2 Background \046 Related Work}{part.1}% 14
\BOOKMARK [1][-]{section.2.1}{2.1 Hoare Logic}{chapter.2}% 15
\BOOKMARK [1][-]{section.2.2}{2.2 Formal Methods For Concurrency}{chapter.2}% 16
\BOOKMARK [1][-]{section.2.3}{2.3 Model Checking}{chapter.2}% 17
\BOOKMARK [1][-]{section.2.4}{2.4 Symbolic Execution}{chapter.2}% 18
\BOOKMARK [1][-]{section.2.5}{2.5 MPI}{chapter.2}% 19
\BOOKMARK [1][-]{section.2.6}{2.6 Model Checkers for MPI}{chapter.2}% 20
\BOOKMARK [1][-]{section.2.7}{2.7 Static Analysis and Runtime Verification for MPI}{chapter.2}% 21
\BOOKMARK [2][-]{subsection.2.7.1}{2.7.1 MPI Static Analyzers}{section.2.7}% 22
\BOOKMARK [2][-]{subsection.2.7.2}{2.7.2 MPI Runtime Verification}{section.2.7}% 23
\BOOKMARK [1][-]{section.2.8}{2.8 Deductive Verification for MPI}{chapter.2}% 24
\BOOKMARK [0][-]{chapter.3}{3 Notation}{part.1}% 25
\BOOKMARK [-1][-]{part.2}{Part II \040Theory}{}% 26
\BOOKMARK [0][-]{chapter.4}{4 The MiniMP Programming Language}{part.2}% 27
\BOOKMARK [1][-]{section.4.1}{4.1 Syntax}{chapter.4}% 28
\BOOKMARK [1][-]{section.4.2}{4.2 The MiniMP Model}{chapter.4}% 29
\BOOKMARK [1][-]{section.4.3}{4.3 Semantics}{chapter.4}% 30
\BOOKMARK [2][-]{subsection.4.3.1}{4.3.1 Process States and Global States}{section.4.3}% 31
\BOOKMARK [2][-]{subsection.4.3.2}{4.3.2 Interpretation}{section.4.3}% 32
\BOOKMARK [2][-]{subsection.4.3.3}{4.3.3 State Space Graph}{section.4.3}% 33
\BOOKMARK [2][-]{subsection.4.3.4}{4.3.4 Actions}{section.4.3}% 34
\BOOKMARK [0][-]{chapter.5}{5 The Specification Language for MiniMP}{part.2}% 35
\BOOKMARK [1][-]{section.5.1}{5.1 Program Segment}{chapter.5}% 36
\BOOKMARK [1][-]{section.5.2}{5.2 Path Predicate}{chapter.5}% 37
\BOOKMARK [1][-]{section.5.3}{5.3 Syntax of The MiniMP Specification Language}{chapter.5}% 38
\BOOKMARK [1][-]{section.5.4}{5.4 Semantics of The MiniMP Contracts}{chapter.5}% 39
\BOOKMARK [1][-]{section.5.5}{5.5 The Collective Triple}{chapter.5}% 40
\BOOKMARK [2][-]{subsection.5.5.1}{5.5.1 The Intuition in Collective Triple}{section.5.5}% 41
\BOOKMARK [2][-]{subsection.5.5.2}{5.5.2 Interference}{section.5.5}% 42
\BOOKMARK [2][-]{subsection.5.5.3}{5.5.3 The Validity of A Collective Triple}{section.5.5}% 43
\BOOKMARK [0][-]{chapter.6}{6 A Inference System for MiniMP}{part.2}% 44
\BOOKMARK [1][-]{section.6.1}{6.1 Rules for Decomposing Collective Triples}{chapter.6}% 45
\BOOKMARK [1][-]{section.6.2}{6.2 The Adaptation Problem}{chapter.6}% 46
\BOOKMARK [1][-]{section.6.3}{6.3 An Derivation Example}{chapter.6}% 47
\BOOKMARK [1][-]{section.6.4}{6.4 Extending the Entering/Exiting Notation}{chapter.6}% 48
\BOOKMARK [1][-]{section.6.5}{6.5 Soundness}{chapter.6}% 49
\BOOKMARK [0][-]{chapter.7}{7 A Verification System for MiniMP}{part.2}% 50
\BOOKMARK [1][-]{section.7.1}{7.1 Symbolic Execution and Model Checking for MiniMP}{chapter.7}% 51
\BOOKMARK [1][-]{section.7.2}{7.2 Composite and Modular Verification for MiniMP}{chapter.7}% 52
\BOOKMARK [2][-]{subsection.7.2.1}{7.2.1 Collective States}{section.7.2}% 53
\BOOKMARK [2][-]{subsection.7.2.2}{7.2.2 The Composite and Modular Verification Algorithm}{section.7.2}% 54
\BOOKMARK [1][-]{section.7.3}{7.3 Procedure Contract System for MiniMP}{chapter.7}% 55
\BOOKMARK [2][-]{subsection.7.3.1}{7.3.1 Formal Parameters and Return Value}{section.7.3}% 56
\BOOKMARK [2][-]{subsection.7.3.2}{7.3.2 On The Fly Model Checking with Collective States}{section.7.3}% 57
\BOOKMARK [2][-]{subsection.7.3.3}{7.3.3 Absence Assertion Verification and Partial Order Reduction}{section.7.3}% 58
\BOOKMARK [2][-]{subsection.7.3.4}{7.3.4 Infinite Reachable States}{section.7.3}% 59
\BOOKMARK [1][-]{section.7.4}{7.4 Soundness}{chapter.7}% 60
\BOOKMARK [2][-]{subsection.7.4.1}{7.4.1 Soundness of The Monolithic Algorithm}{section.7.4}% 61
\BOOKMARK [2][-]{subsection.7.4.2}{7.4.2 Soundness of The Composite And Modular Algorithm }{section.7.4}% 62
\BOOKMARK [-1][-]{part.3}{Part III \040Practice}{}% 63
\BOOKMARK [0][-]{chapter.8}{8 Modeling C/MPI Programs in The CIVL Framework}{part.3}% 64
\BOOKMARK [1][-]{section.8.1}{8.1 CIVL: The Concurrency Intermediate Verification Language}{chapter.8}% 65
\BOOKMARK [1][-]{section.8.2}{8.2 Modeling MPI with Transformation and Libraries}{chapter.8}% 66
\BOOKMARK [2][-]{subsection.8.2.1}{8.2.1 The MPI Library}{section.8.2}% 67
\BOOKMARK [2][-]{subsection.8.2.2}{8.2.2 AST-Level Code Transformation}{section.8.2}% 68
\BOOKMARK [2][-]{subsection.8.2.3}{8.2.3 MPI Program Properties}{section.8.2}% 69
\BOOKMARK [0][-]{chapter.9}{9 Verifying C/MPI Programs with Function Contracts}{part.3}% 70
\BOOKMARK [1][-]{section.9.1}{9.1 Bring Function Contracts From MiniMP To MPI}{chapter.9}% 71
\BOOKMARK [1][-]{section.9.2}{9.2 The MPI Contract Language}{chapter.9}% 72
\BOOKMARK [2][-]{subsection.9.2.1}{9.2.1 Syntax}{section.9.2}% 73
\BOOKMARK [2][-]{subsection.9.2.2}{9.2.2 Semantics}{section.9.2}% 74
\BOOKMARK [1][-]{section.9.3}{9.3 MPI Function Contract System Implementation}{chapter.9}% 75
\BOOKMARK [2][-]{subsection.9.3.1}{9.3.1 Implementing Collates}{section.9.3}% 76
\BOOKMARK [2][-]{subsection.9.3.2}{9.3.2 Implementing Absence Assertions}{section.9.3}% 77
\BOOKMARK [2][-]{subsection.9.3.3}{9.3.3 Transformation}{section.9.3}% 78
\BOOKMARK [0][-]{chapter.10}{10 Evaluation}{part.3}% 79
\BOOKMARK [1][-]{section.10.1}{10.1 Running Examples}{chapter.10}% 80
\BOOKMARK [2][-]{subsection.10.1.1}{10.1.1 Allgather Implementations}{section.10.1}% 81
\BOOKMARK [2][-]{subsection.10.1.2}{10.1.2 Parallel Vector Product}{section.10.1}% 82
\BOOKMARK [1][-]{section.10.2}{10.2 Experiment}{chapter.10}% 83
\BOOKMARK [0][-]{chapter.11}{11 Summary and Future Work}{part.3}% 84
\BOOKMARK [1][-]{section.11.1}{11.1 Dissertation Summary}{chapter.11}% 85
\BOOKMARK [1][-]{section.11.2}{11.2 Future Work}{chapter.11}% 86
\BOOKMARK [0][-]{chapter*.61}{Bibliography}{part.3}% 87