\relax 
\providecommand\hyper@newdestlabel[2]{}
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax 
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\@input{template.aux}
\providecommand \oddpage@label [2]{}
\@writefile{toc}{\contentsline {part}{Part\ \numberline {I}\uppercase {$\nobreakspace  {}$Preliminaries}}{1}{part.1}}
\citation{bernholdt-etal:2018:mpi_exascale}
\citation{mpi-forum:2015:mpi31}
\citation{johansen:2017:earthquake}
\citation{drake:2005:overview}
\citation{valiev:2010:nwchem}
\citation{mathuriya:2017:embracingquantum}
\@writefile{toc}{\contentsline {chapter}{\numberline {1}Introduction}{2}{chapter.1}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:intro}{{1}{2}{Introduction}{chapter.1}{}}
\@writefile{toc}{\contentsline {section}{\numberline {1.1}Motivation}{2}{section.1.1}}
\citation{gopalakrishnan-etal:2017:correctness,correctness:2017:proceedings,correctness:2018:proceedings,hatton:1997:T_Experiments,hatton-roberts:1994:accurate,hatton:2012:defects,merali:2010:error}
\citation{Meyer:1992:ADC}
\citation{Meyer:1988:eiffel}
\citation{vandevoorde:1994:specializedprocedures}
\citation{leavens:1999:jml}
\citation{spark}
\citation{ada2012}
\citation{ACSL:Reference}
\citation{hoare:1969:axiomatic}
\citation{araujo:2011:enabling,rebelo:2014:aspectjml}
\citation{zheng:2008:test,krenn:2009:test}
\citation{Z3Prover,barrett-etal:2011:cvc4,alt-ergo,kovacs:2013:firstorder}
\citation{barnett:2006:boogie,gordon:1989:mechanizing,leino:1999:checkingjava,dannenberg:1982:formal,cuoq:2011:wp,filliatre:2013:why3,leino:2010:dafny,ball:2010:towards,barnett:2005:specsharp,beckert:2007:KeY}
\citation{cohen-etal:2009:vcc,blom:2017:vercors,amani:2017:complex}
\citation{bernholdt-etal:2018:mpi_exascale}
\citation{romano-etal:2015:openmc}
\citation{yang-etal:2017:amg}
\@writefile{toc}{\contentsline {section}{\numberline {1.2}Contributions}{5}{section.1.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.1}A contract theory for message-passing programs}{5}{subsection.1.2.1}}
\citation{clarke:2000:modelchecking,mcmillan:1993:symbolic}
\citation{king:1976:symbolic,clarke:1976:symbolically}
\citation{Jackson:2006:SAL,biere:2003:bounded,kroening:2014:cbmc}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.2}A method for verifying collective contracts}{6}{subsection.1.2.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.3}An MPI Specification Language}{7}{subsection.1.2.3}}
\citation{siegel-etal:2015:civl_sc,zheng-etal:2016:civl_tacas,zheng-etal:2015:civl_ase}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2.4}A Prototype MPI Contract-Based Verification Tool}{8}{subsection.1.2.4}}
\@writefile{toc}{\contentsline {section}{\numberline {1.3}Outline}{8}{section.1.3}}
\citation{hoare:1969:axiomatic}
\@writefile{toc}{\contentsline {chapter}{\numberline {2}Background \& Related Work}{10}{chapter.2}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:background-related}{{2}{10}{Background \& Related Work}{chapter.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {2.1}Hoare Logic}{10}{section.2.1}}
\newlabel{sec:background:hoarelogic}{{2.1}{10}{Hoare Logic}{section.2.1}{}}
\citation{barnett:2006:boogie,gordon:1989:mechanizing,leino:1999:checkingjava}
\citation{Meyer:1992:ADC}
\citation{Meyer:1988:eiffel}
\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Inference rules of Hoare calculus.\relax }}{12}{figure.caption.7}}
\providecommand*\caption@xref[2]{\@setref\relax\@undefined{#1}}
\newlabel{fig:intro:hoare:rules}{{2.1}{12}{Inference rules of Hoare calculus.\relax }{figure.caption.7}{}}
\citation{filliatre:2013:why3}
\citation{barnett:2006:boogie}
\citation{Gosling:2014:JLS:2636997}
\citation{barnett:2005:specsharp}
\citation{Barnes:2012:SPA}
\citation{leino:2010:dafny}
\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces The derivation of a Hoare triple. $X$ and $Y$ are auxiliary variables holding the values of \texttt  {x} and \texttt  {y}, respectively, at pre-state. The symbol $\mathit  {abs}$ represents the absolute value function in the underlying first order logic. \relax }}{13}{figure.caption.8}}
\newlabel{fig:intro:hoare:derive}{{2.2}{13}{The derivation of a Hoare triple. $X$ and $Y$ are auxiliary variables holding the values of \texttt {x} and \texttt {y}, respectively, at pre-state. The symbol $\mymath {abs}$ represents the absolute value function in the underlying first order logic. \relax }{figure.caption.8}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {2.3}{\ignorespaces The computation of the weakest pre-condition, $\textup  {WP}(S, Q)$, for a given statement $S$ and desired post-condition $Q$. \relax }}{13}{figure.caption.9}}
\newlabel{fig:intro:hoare:wp}{{2.3}{13}{The computation of the weakest pre-condition, $\textup {WP}(S, Q)$, for a given statement $S$ and desired post-condition $Q$. \relax }{figure.caption.9}{}}
\citation{lahiri2012security,ball:2010:towards}
\citation{spark}
\citation{cuoq2012framac}
\citation{cuoq:2011:wp}
\citation{Owicki1976}
\citation{lamport:1980:hoare}
\citation{Takaoka:1994:PPV:326619.326811}
\citation{Owicki1976}
\@writefile{toc}{\contentsline {section}{\numberline {2.2}Formal Methods For Concurrency}{14}{section.2.2}}
\newlabel{sec:background:formal4concurrency}{{2.2}{14}{Formal Methods For Concurrency}{section.2.2}{}}
\citation{lamport:1980:hoare}
\citation{Takaoka:1994:PPV:326619.326811}
\citation{Newton1975}
\citation{Newton1975}
\citation{Ashcroft:1975:PAP:1739967.1740302}
\citation{Ashcroft:1975:PAP:1739967.1740302}
\citation{Floyd1993}
\citation{Manna:1984:APP:2731.2734}
\citation{Owicki:1982:PLP:357172.357178}
\citation{Stark:1985:PTR:646823.706907}
\citation{cohen-etal:2009:vcc}
\citation{amani:2017:complex}
\citation{beckert:2007:KeY}
\citation{leino:2009:verification}
\citation{Jacobs:2010:QTV:1947873.1947902}
\citation{Gosling:2014:JLS:2636997}
\citation{reynolds2002separation}
\citation{clarke:2000:modelchecking}
\citation{Siegel:2005:MWM:1065944.1065957,10.1007/978-3-540-30579-8_27,siegel2007verifying}
\@writefile{toc}{\contentsline {section}{\numberline {2.3}Model Checking}{17}{section.2.3}}
\newlabel{sec:background:modelchecking}{{2.3}{17}{Model Checking}{section.2.3}{}}
\citation{Jackson:2006:SAL}
\citation{godefroid:1993:refining,10.1007/BFb0013032,Valmari1992}
\citation{king:1976:symbolic}
\@writefile{toc}{\contentsline {section}{\numberline {2.4}Symbolic Execution}{18}{section.2.4}}
\newlabel{sec:background:symexe}{{2.4}{18}{Symbolic Execution}{section.2.4}{}}
\citation{Z3Prover,barrett-etal:2011:cvc4,alt-ergo}
\newlabel{exmp:intro:symexe}{{2.2}{19}{}{thm.2.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {2.5}MPI}{19}{section.2.5}}
\newlabel{sec:background:mpi}{{2.5}{19}{MPI}{section.2.5}{}}
\citation{clarke:2000:modelchecking}
\citation{vakkalanka2008dynamic}
\citation{Vo:2010:SDD:1884643.1884681}
\@writefile{lof}{\contentsline {figure}{\numberline {2.4}{\ignorespaces A simple C/MPI program. Process 0 sends and process 1 receives a message. The remaining processes perform no operation.\relax }}{21}{figure.caption.10}}
\newlabel{fig:mpi:simple}{{2.4}{21}{A simple C/MPI program. Process 0 sends and process 1 receives a message. The remaining processes perform no operation.\relax }{figure.caption.10}{}}
\@writefile{toc}{\contentsline {section}{\numberline {2.6}Model Checkers for MPI}{21}{section.2.6}}
\newlabel{sec:related:modelcheckers}{{2.6}{21}{Model Checkers for MPI}{section.2.6}{}}
\citation{king:1976:symbolic}
\citation{Yu:2018:CSE:3183440.3190336}
\citation{Hoare:1985:CSP:3921}
\citation{Forejt:2017:PPA:3133234.3095075}
\citation{khanna2018dynamic}
\citation{siegel2007verifying}
\citation{siegel2011tass}
\citation{Luo:2017:VMP:3127024.3127032}
\citation{holzmann1997spin}
\citation{Luo:2017:VMP:3127024.3127032}
\citation{Droste:2015:MSA:2833157.2833159}
\citation{clangstaticanalyzer}
\citation{christakis:2011:detection}
\citation{armstrong:2013:programming}
\@writefile{toc}{\contentsline {section}{\numberline {2.7}Static Analysis and Runtime Verification for MPI}{24}{section.2.7}}
\newlabel{sec:related:staticanalyzer}{{2.7}{24}{Static Analysis and Runtime Verification for MPI}{section.2.7}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.7.1}MPI Static Analyzers}{24}{subsection.2.7.1}}
\citation{huchant2019multivalued}
\citation{Bronevetsky:2009:CSD:1545006.1545049,Strout:2006:DAM:1156433.1157634}
\citation{ye:2018:detecting}
\citation{board:1993:ieee}
\citation{ye:2018:detecting}
\citation{ye:2018:detecting}
\citation{ye:2018:detecting}
\citation{ye:2018:detecting}
\citation{krammer2004marmot}
\citation{Hilbrich:2012:MRE:2388996.2389037}
\@writefile{toc}{\contentsline {subsection}{\numberline {2.7.2}MPI Runtime Verification}{26}{subsection.2.7.2}}
\citation{Lopez:2015:PVM:2814270.2814302}
\citation{cohen-etal:2009:vcc}
\citation{oortwijn2016future}
\citation{bergstra2001handbook}
\citation{Cranen:2013:OMT:2450387.2450410}
\@writefile{toc}{\contentsline {section}{\numberline {2.8}Deductive Verification for MPI}{27}{section.2.8}}
\newlabel{sec:related:deductive}{{2.8}{27}{Deductive Verification for MPI}{section.2.8}{}}
\citation{luo2018towards}
\citation{Ashcroft:1975:PAP:1739967.1740302}
\@writefile{toc}{\contentsline {chapter}{\numberline {3}Notation}{29}{chapter.3}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:notation}{{3}{29}{Notation}{chapter.3}{}}
\@writefile{toc}{\contentsline {part}{Part\ \numberline {II}\uppercase {$\nobreakspace  {}$Theory}}{31}{part.2}}
\newlabel{part:2}{{II}{32}{$~$Theory}{part.2}{}}
\@writefile{toc}{\contentsline {chapter}{\numberline {4}The MiniMP Programming Language}{32}{chapter.4}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:minimp}{{4}{32}{The MiniMP Programming Language}{chapter.4}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4.1}Syntax}{32}{section.4.1}}
\newlabel{sec:minimp:syntax}{{4.1}{32}{Syntax}{section.4.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.1}{\ignorespaces The grammar of \textsc  {MiniMP}{}. An \texttt  {\texttt  {\textit  {\leavevmode {\color  {blue}Identifier}}}} is a character sequences. An \texttt  {\texttt  {\textit  {\leavevmode {\color  {blue}IntegerLiteral}}}} is an integer literal. An \texttt  {\texttt  {\char `\{}{} \texttt  {\textit  {\leavevmode {\color  {blue}List-of-Constant}}} \texttt  {\char `\}}{}} is an array literal.\relax }}{33}{figure.caption.11}}
\newlabel{fig:minimp:syntax}{{4.1}{33}{The grammar of \minimp {}. An \texttt {\nonterm {Identifier}} is a character sequences. An \texttt {\nonterm {IntegerLiteral}} is an integer literal. An \texttt {\lb {} \nonterm {List-of-Constant} \rb {}} is an array literal.\relax }{figure.caption.11}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.2}{\ignorespaces A \textsc  {MiniMP}{} program in which the \texttt  {main} procedure (right) uses the \texttt  {bcast} procedure (left). By the end of an execution of this program, each process will have value ``$0$'' in its variable \texttt  {buf}.\relax }}{35}{figure.caption.12}}
\newlabel{fig:minimp:example:bcast}{{4.2}{35}{A \minimp {} program in which the \texttt {main} procedure (right) uses the \texttt {bcast} procedure (left). By the end of an execution of this program, each process will have value ``$0$'' in its variable \texttt {buf}.\relax }{figure.caption.12}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4.2}The \textsc  {MiniMP}{} Model}{35}{section.4.2}}
\newlabel{sec:minimp:model}{{4.2}{35}{The \minimp {} Model}{section.4.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.3}{\ignorespaces A \textsc  {MiniMP}{} program in which the \texttt  {main} procedure (right) uses the \texttt  {gather} procedure (left). By the end of an execution of this program with $n$ processes, the process 0 will have a sequence of values ``$012\ldots  {}(n-1)$'' in its variable \texttt  {result}.\relax }}{36}{figure.caption.13}}
\newlabel{fig:minimp:example:gather}{{4.3}{36}{A \minimp {} program in which the \texttt {main} procedure (right) uses the \texttt {gather} procedure (left). By the end of an execution of this program with $n$ processes, the process 0 will have a sequence of values ``$012\ldots {}(n-1)$'' in its variable \texttt {result}.\relax }{figure.caption.13}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.4}{\ignorespaces A \textsc  {MiniMP}{} program where the \texttt  {main} procedure (right) uses a \texttt  {scatter} procedure (left). By the end of an execution of this program, the process $i$ will have value ``$i$'' in its variable \texttt  {result}.\relax }}{36}{figure.caption.14}}
\newlabel{fig:minimp:example:scatter}{{4.4}{36}{A \minimp {} program where the \texttt {main} procedure (right) uses a \texttt {scatter} procedure (left). By the end of an execution of this program, the process $i$ will have value ``$i$'' in its variable \texttt {result}.\relax }{figure.caption.14}{}}
\newlabel{defn:expr-and-bexpr}{{4.5}{37}{}{thm.4.5}{}}
\newlabel{defn:function-graph}{{4.7}{38}{}{thm.4.7}{}}
\newlabel{defn:model}{{4.9}{39}{}{thm.4.9}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.5}{\ignorespaces The pseudocode definition of the translation process.\relax }}{40}{figure.caption.15}}
\newlabel{fig:minimp:translation}{{4.5}{40}{The pseudocode definition of the translation process.\relax }{figure.caption.15}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.6}{\ignorespaces Procedure graph of the \texttt  {bcast} procedure in Fig.\ \ref  {fig:minimp:example:bcast}. Boxes are program locations. Arrows are labeled by an atomic statement and a guard (in red). Trivial statement \textsf  {skip}{} and trivial guard \texttt  {true} are omitted. Two boxes, including the arrow that connects them, represent a local transition. The bold boxes $0$ and ${12}$ are the sole entry and exit, respectively.\relax }}{41}{figure.caption.16}}
\newlabel{fig:exmp:func-graph}{{4.6}{41}{Procedure graph of the \texttt {bcast} procedure in Fig.\^^M\ref {fig:minimp:example:bcast}. Boxes are program locations. Arrows are labeled by an atomic statement and a guard (in red). Trivial statement \myskipstmt {} and trivial guard \texttt {true} are omitted. Two boxes, including the arrow that connects them, represent a local transition. The bold boxes $0$ and ${12}$ are the sole entry and exit, respectively.\relax }{figure.caption.16}{}}
\@writefile{toc}{\contentsline {section}{\numberline {4.3}Semantics}{41}{section.4.3}}
\newlabel{sec:minimp:semantics}{{4.3}{41}{Semantics}{section.4.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.1}Process States and Global States}{41}{subsection.4.3.1}}
\newlabel{defn:domain}{{4.10}{41}{}{thm.4.10}{}}
\newlabel{page:notation:procState}{{4.3.1}{43}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:stack}{{4.3.1}{43}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:top}{{4.3.1}{43}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:toploc}{{4.3.1}{43}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:mem}{{4.3.1}{43}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:comm}{{4.3.1}{43}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:push}{{4.3.1}{43}{Process States and Global States}{thm.4.13}{}}
\citation{Hoare:1985:CSP:3921}
\newlabel{page:notation:pop}{{4.3.1}{44}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:assign}{{4.3.1}{44}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:enque}{{4.3.1}{44}{Process States and Global States}{thm.4.13}{}}
\newlabel{page:notation:deque}{{4.3.1}{44}{Process States and Global States}{thm.4.13}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.2}Interpretation}{44}{subsection.4.3.2}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.7}{\ignorespaces \textsc  {MiniMP}{} expression evaluation, where $s$ is a state, $p$ is a process, $v$ is a variable, $e, e_0, e_1$ are expressions. The \textsf  {bop} stands for a binary operator (e.g., \texttt  {+, -, $\ldots  {}$}). The \textsf  {uop} stands for a unary operator (e.g., \texttt  {!, -, $\ldots  {}$}). \relax }}{45}{figure.caption.17}}
\newlabel{fig:minimp:eval:semantics}{{4.7}{45}{\minimp {} expression evaluation, where $s$ is a state, $p$ is a process, $v$ is a variable, $e, e_0, e_1$ are expressions. The \textsf {bop} stands for a binary operator (e.g., \texttt {+, -, $\ldots {}$}). The \textsf {uop} stands for a unary operator (e.g., \texttt {!, -, $\ldots {}$}). \relax }{figure.caption.17}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {4.8}{\ignorespaces The definition of the $n$-processes interpretation function $\mathit  {I_n}$ that describes the results of executing a local transition from a state by a process.\relax }}{46}{figure.caption.18}}
\newlabel{fig:minimp:interpretation}{{4.8}{46}{The definition of the $n$-processes interpretation function $\mymath {I_n}$ that describes the results of executing a local transition from a state by a process.\relax }{figure.caption.18}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.3}State Space Graph}{47}{subsection.4.3.3}}
\newlabel{page:term:reachable}{{4.3.3}{48}{State Space Graph}{thm.4.17}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.4}Actions}{49}{subsection.4.3.4}}
\newlabel{page:term:state-space}{{4.3.4}{50}{Actions}{thm.4.24}{}}
\citation{lamport:1980:hoare}
\@writefile{toc}{\contentsline {chapter}{\numberline {5}The Specification Language for MiniMP}{51}{chapter.5}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:minimp:spec}{{5}{51}{The Specification Language for MiniMP}{chapter.5}{}}
\@writefile{toc}{\contentsline {section}{\numberline {5.1}Program Segment}{51}{section.5.1}}
\newlabel{sec:minimp:spec:progseg}{{5.1}{51}{Program Segment}{section.5.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {5.1}{\ignorespaces The program segment of the loop \texttt  {\textit  {\leavevmode {\color  {blue}Statement}}} in the \texttt  {bcast} procedure showed in Fig.\ \ref  {fig:minimp:example:bcast}.\relax }}{53}{figure.caption.19}}
\newlabel{fig:program:segment:visual}{{5.1}{53}{The program segment of the loop \nonterm {Statement} in the \texttt {bcast} procedure showed in Fig.\^^M\ref {fig:minimp:example:bcast}.\relax }{figure.caption.19}{}}
\citation{dwyer:1999:patterns}
\citation{dwyer:1999:patterns}
\@writefile{toc}{\contentsline {section}{\numberline {5.2}Path Predicate}{55}{section.5.2}}
\newlabel{sec:minimp:spec:path}{{5.2}{55}{Path Predicate}{section.5.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {5.3}Syntax of The \textsc  {MiniMP}{} Specification Language}{55}{section.5.3}}
\newlabel{sec:minimp:spec:syntax}{{5.3}{55}{Syntax of The \minimp {} Specification Language}{section.5.3}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {5.2}{\ignorespaces The syntax of \textsc  {MiniMP}{} specification language\relax }}{56}{figure.caption.20}}
\newlabel{fig:minimp-spec-expr}{{5.2}{56}{The syntax of \minimp {} specification language\relax }{figure.caption.20}{}}
\newlabel{rest:absent:1}{{5.10}{57}{}{Item.32}{}}
\@writefile{toc}{\contentsline {section}{\numberline {5.4}Semantics of The \textsc  {MiniMP}{} Contracts}{58}{section.5.4}}
\newlabel{sec:minimp:spec:semantics}{{5.4}{58}{Semantics of The \minimp {} Contracts}{section.5.4}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {5.3}{\ignorespaces  The definition of the $n$-processes specification evaluation function $[\tmspace  -\thinmuskip {.1667em}[\mathit  {e}]\tmspace  -\thinmuskip {.1667em}]^{\textsf  {spec}}_n$, which evaluates a contract expression $e$ for a process $p$ at a pre- or a post-state $s$ of a program segment $l{\penalty \@M \mskip 2mu\mathpunct {}\nonscript \mkern -\thinmuskip {:}\mskip 6muplus1mu\relax }C\nobreakspace  {}{l'}$ in a path $\rho $.\relax }}{59}{figure.caption.21}}
\newlabel{fig:spec:expr:eval}{{5.3}{59}{The definition of the $n$-processes specification evaluation function $\myseval {e}_n$, which evaluates a contract expression $e$ for a process $p$ at a pre- or a post-state $s$ of a program segment $\progseg {l}{C}{l'}$ in a path $\rho $.\relax }{figure.caption.21}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {5.4}{\ignorespaces The definition of the event interpretation function $\mathit  {I^{\textsf  {event}}_{C, \rho }}$ with respect to a path $\rho $ and a program segment $l{\penalty \@M \mskip 2mu\mathpunct {}\nonscript \mkern -\thinmuskip {:}\mskip 6muplus1mu\relax }C\nobreakspace  {}{l'}$.\relax }}{60}{figure.caption.22}}
\newlabel{fig:event:interpret}{{5.4}{60}{The definition of the event interpretation function $\mymath {I^{\textsf {event}}_{C, \rho }}$ with respect to a path $\rho $ and a program segment $\progseg {l}{C}{l'}$.\relax }{figure.caption.22}{}}
\newlabel{exmp:minimp:spec:gather}{{5.16}{61}{}{thm.5.16}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {5.5}{\ignorespaces A contract of a branch statement that ``broadcasts'' a value.\relax }}{62}{figure.caption.23}}
\newlabel{fig:minimp:spec:bcast}{{5.5}{62}{A contract of a branch statement that ``broadcasts'' a value.\relax }{figure.caption.23}{}}
\@writefile{toc}{\contentsline {section}{\numberline {5.5}The Collective Triple}{62}{section.5.5}}
\newlabel{sec:minimp:spec:triple}{{5.5}{62}{The Collective Triple}{section.5.5}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {5.6}{\ignorespaces A contract for the branch statement that ``gathers'' values from all processes.\relax }}{63}{figure.caption.24}}
\newlabel{fig:minimp:spec:gather}{{5.6}{63}{A contract for the branch statement that ``gathers'' values from all processes.\relax }{figure.caption.24}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.1}The Intuition in Collective Triple}{64}{subsection.5.5.1}}
\@writefile{lof}{\contentsline {figure}{\numberline {5.7}{\ignorespaces A \textsc  {MiniMP}{} program in pseudocode where \textit  {init} is a procedure that depends on \texttt  {PID} and initializes \texttt  {dat} elements. Suppose \texttt  {\textit  {barrier}} is a barrier.\relax }}{65}{figure.caption.25}}
\newlabel{fig:minimp:example:exchanges}{{5.7}{65}{A \minimp {} program in pseudocode where \textit {init} is a procedure that depends on \texttt {PID} and initializes \texttt {dat} elements. Suppose \texttt {\textit {barrier}} is a barrier.\relax }{figure.caption.25}{}}
\newlabel{exmp:minimp:ideal:reasoning}{{5.19}{65}{}{thm.5.19}{}}
\newlabel{defn:extended:execution}{{5.20}{67}{}{Item.39}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.2}Interference}{67}{subsection.5.5.2}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5.3}The Validity of A Collective Triple}{69}{subsection.5.5.3}}
\newlabel{defn:semantics:collective:triple}{{5.23}{69}{}{Item.43}{}}
\@writefile{toc}{\contentsline {chapter}{\numberline {6}A Inference System for MiniMP}{70}{chapter.6}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:minimp:rules}{{6}{70}{A Inference System for MiniMP}{chapter.6}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6.1}Rules for Decomposing Collective Triples}{70}{section.6.1}}
\newlabel{sec:minimp:spec:rule}{{6.1}{70}{Rules for Decomposing Collective Triples}{section.6.1}{}}
\newlabel{defn:guarantee:assertion}{{6.3}{72}{}{thm.6.3}{}}
\newlabel{defn:nosend:subset}{{6.4}{72}{}{Item.47}{}}
\newlabel{defn:infer:togather}{{6.5}{73}{}{thm.6.5}{}}
\newlabel{defn:nocancel}{{6.6}{73}{}{thm.6.6}{}}
\newlabel{defn:path:equivalence}{{6.7}{74}{}{thm.6.7}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {6.1}{\ignorespaces Rules for decomposing collective triples\relax }}{75}{figure.caption.26}}
\newlabel{fig:triple:rules}{{6.1}{75}{Rules for decomposing collective triples\relax }{figure.caption.26}{}}
\citation{hoare:1969:axiomatic,Kleymann:1999:HLA:2769784.2769811}
\@writefile{toc}{\contentsline {section}{\numberline {6.2}The Adaptation Problem}{77}{section.6.2}}
\newlabel{sec:minimp:spec:rule:adaptation}{{6.2}{77}{The Adaptation Problem}{section.6.2}{}}
\newlabel{exam:minimp:rule:adaptation}{{6.10}{77}{}{thm.6.10}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6.3}An Derivation Example}{78}{section.6.3}}
\newlabel{sec:rules:example}{{6.3}{78}{An Derivation Example}{section.6.3}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {6.2}{\ignorespaces A contract for the sequential combination of the two branch statements given by Fig.\ \ref  {fig:minimp:spec:gather} and \ref  {fig:minimp:spec:bcast}.\relax }}{79}{figure.caption.27}}
\newlabel{fig:minimp:corule:example:1}{{6.2}{79}{A contract for the sequential combination of the two branch statements given by Fig.\ \ref {fig:minimp:spec:gather} and \ref {fig:minimp:spec:bcast}.\relax }{figure.caption.27}{}}
\@writefile{toc}{\contentsline {section}{\numberline {6.4}Extending the Entering/Exiting Notation}{79}{section.6.4}}
\newlabel{sec:extended:enter:exit}{{6.4}{79}{Extending the Entering/Exiting Notation}{section.6.4}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {6.3}{\ignorespaces A $\mathcal  {R}$ derivation of a collective triple that specifies a sequential combination of two collective style \textsc  {MiniMP}{} statements. \relax }}{80}{figure.caption.28}}
\newlabel{fig:minimp:corule:apply:1}{{6.3}{80}{A $\corule $ derivation of a collective triple that specifies a sequential combination of two collective style \minimp {} statements. \relax }{figure.caption.28}{}}
\citation{lipton:reduction}
\@writefile{toc}{\contentsline {section}{\numberline {6.5}Soundness}{81}{section.6.5}}
\newlabel{sec:rules:soundness}{{6.5}{81}{Soundness}{section.6.5}{}}
\newlabel{lema:base}{{6.13}{81}{}{thm.6.13}{}}
\newlabel{lema:gen:non-interfere-sufficient}{{6.14}{82}{}{thm.6.14}{}}
\newlabel{coro:pre:post:alternative}{{6.15}{83}{}{Item.49}{}}
\newlabel{lema:seq:reproduce}{{6.16}{83}{}{Item.53}{}}
\newlabel{lema:seq}{{6.17}{84}{soundness of the sequence rule}{thm.6.17}{}}
\newlabel{lema:seq:zero}{{6.18}{84}{}{thm.6.18}{}}
\newlabel{lema:seq:one}{{6.19}{86}{}{thm.6.19}{}}
\newlabel{lema:seq:two}{{6.20}{86}{}{thm.6.20}{}}
\newlabel{lema:seq:two:proof:a}{{{a}}{86}{Soundness}{equation.6.5.1}{}}
\newlabel{lema:seq:two:proof:caseone:b}{{{b}}{87}{Soundness}{equation.6.5.1}{}}
\newlabel{lema:seq:two:casetwo:c}{{{c}}{87}{Soundness}{equation.6.5.1}{}}
\newlabel{lema:seq:two:casetwoone:d}{{{d}}{88}{Soundness}{equation.6.5.1}{}}
\newlabel{lema:seq:two:casetwotwo:e}{{{e}}{88}{Soundness}{equation.6.5.1}{}}
\newlabel{lema:seq:two:casetwotwotwo:f}{{{f}}{88}{Soundness}{equation.6.5.1}{}}
\newlabel{lema:seq:two:casetwotwotwo:g}{{{g}}{88}{Soundness}{equation.6.5.1}{}}
\newlabel{lema:seq:three}{{6.21}{89}{}{thm.6.21}{}}
\newlabel{lema:three:proof:a}{{{a}}{89}{Soundness}{thm.6.21}{}}
\newlabel{lema:three:proof:b}{{{b}}{90}{Soundness}{thm.6.21}{}}
\newlabel{lema:three:proof:c}{{{c}}{90}{Soundness}{Item.61}{}}
\newlabel{lema:three:proof:d}{{{d}}{90}{Soundness}{Item.62}{}}
\newlabel{lema:three:proof:e}{{{e}}{90}{Soundness}{Item.62}{}}
\newlabel{lema:three:proof:f}{{{f}}{91}{Soundness}{Item.62}{}}
\newlabel{lema:conseq}{{6.22}{91}{soundness of the consequence rule}{thm.6.22}{}}
\newlabel{lema:loop}{{6.23}{91}{soundness of the collective loop rule}{thm.6.23}{}}
\newlabel{lema:elab}{{6.24}{92}{soundness of the elaboration rule}{thm.6.24}{}}
\@writefile{toc}{\contentsline {chapter}{\numberline {7}A Verification System for MiniMP}{93}{chapter.7}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:minimp:system}{{7}{93}{A Verification System for MiniMP}{chapter.7}{}}
\@writefile{toc}{\contentsline {section}{\numberline {7.1}Symbolic Execution and Model Checking for \textsc  {MiniMP}{}}{93}{section.7.1}}
\newlabel{sec:minimp:system:symExe}{{7.1}{93}{Symbolic Execution and Model Checking for \minimp {}}{section.7.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7.1}{\ignorespaces The definition of the interpretation for symbolic execution with $n$ processes.\relax }}{94}{figure.caption.29}}
\newlabel{fig:minimp:system:interpretation}{{7.1}{94}{The definition of the interpretation for symbolic execution with $n$ processes.\relax }{figure.caption.29}{}}
\newlabel{defn:mayinterfere}{{7.7}{97}{}{thm.7.7}{}}
\newlabel{defn:minimp:mono:error}{{7.8}{97}{}{thm.7.8}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7.2}{\ignorespaces The definition of contract violation and deadlock for a prefix $\rho $ of an execution in the state space graph $G$ searched by $\textsc  {Mc}(\mathcal  {M}, \delimiter "426830A {}\psi ,\tmspace  +\thinmuskip {.1667em}\Gamma {}\delimiter "526930B {}\nobreakspace  {}C\nobreakspace  {}\delimiter "426830A {}\phi ,\tmspace  +\thinmuskip {.1667em}\Upsilon {}\delimiter "526930B {}{}, n)$.\relax }}{98}{figure.caption.30}}
\newlabel{fig:minimp:mono:error}{{7.2}{98}{The definition of contract violation and deadlock for a prefix $\rho $ of an execution in the state space graph $G$ searched by $\mcalgo (\model , \cotriplenoloc {}, n)$.\relax }{figure.caption.30}{}}
\@writefile{toc}{\contentsline {section}{\numberline {7.2}Composite and Modular Verification for \textsc  {MiniMP}{}}{98}{section.7.2}}
\newlabel{sec:minimp:system:symExeModular}{{7.2}{98}{Composite and Modular Verification for \minimp {}}{section.7.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.1}Collective States}{99}{subsection.7.2.1}}
\newlabel{subsec:collective:state}{{7.2.1}{99}{Collective States}{subsection.7.2.1}{}}
\newlabel{defn:collective:state}{{7.13}{101}{}{thm.7.13}{}}
\newlabel{exmp:collective:state}{{7.14}{102}{}{thm.7.14}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.2}The Composite and Modular Verification Algorithm}{102}{subsection.7.2.2}}
\newlabel{subsec:modular:algorihtm}{{7.2.2}{102}{The Composite and Modular Verification Algorithm}{subsection.7.2.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7.3}{\ignorespaces A collective state (upper right) associated with an execution (below) of a \textsc  {MiniMP}{} program (upper left). All processes are collectively at line 6 in the collective state.\relax }}{103}{figure.caption.31}}
\newlabel{fig:minimp:example:collective:state}{{7.3}{103}{A collective state (upper right) associated with an execution (below) of a \minimp {} program (upper left). All processes are collectively at line 6 in the collective state.\relax }{figure.caption.31}{}}
\newlabel{defn:modular:verification:infeasible}{{7.19}{105}{}{Item.77}{}}
\newlabel{defn:modular:verify:error}{{7.21}{106}{}{thm.7.21}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7.4}{\ignorespaces Conditions of a contract violation of an execution $\pi $ explored by $\textsc  {Mc}^{\Delta }(\mathcal  {M}, \frac  {\textsf  {Tri}}{\delimiter "426830A {}\psi ,\tmspace  +\thinmuskip {.1667em}\Gamma {}\delimiter "526930B {}\nobreakspace  {}C\nobreakspace  {}\delimiter "426830A {}\phi ,\tmspace  +\thinmuskip {.1667em}\Upsilon {}\delimiter "526930B {}{}}, n)$.\relax }}{107}{figure.caption.32}}
\newlabel{fig:modular:verify:error}{{7.4}{107}{Conditions of a contract violation of an execution $\pi $ explored by $\mcalgo ^{\Delta }(\model , \frac {\textsf {Tri}}{\cotriplenoloc {}}, n)$.\relax }{figure.caption.32}{}}
\@writefile{toc}{\contentsline {section}{\numberline {7.3}Procedure Contract System for \textsc  {MiniMP}{}}{108}{section.7.3}}
\newlabel{sec:minimp:modular:system}{{7.3}{108}{Procedure Contract System for \minimp {}}{section.7.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.1}Formal Parameters and Return Value}{109}{subsection.7.3.1}}
\newlabel{sec:minimp:system:formal:return}{{7.3.1}{109}{Formal Parameters and Return Value}{subsection.7.3.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7.5}{\ignorespaces A \textsc  {MiniMP}{} procedure \texttt  {exchange} and its contract.\relax }}{111}{figure.caption.33}}
\newlabel{fig:minimp:contract:example:exchange}{{7.5}{111}{A \minimp {} procedure \texttt {exchange} and its contract.\relax }{figure.caption.33}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.2}On The Fly Model Checking with Collective States}{111}{subsection.7.3.2}}
\newlabel{sec:minimp:system:onthefly}{{7.3.2}{111}{On The Fly Model Checking with Collective States}{subsection.7.3.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7.6}{\ignorespaces The structure of a collate type object for $n$ processes. \textsf  {id} denotes the identifier of the associated procedure, \textsf  {tag} indicates whether the collate serves for a collective pre- or post-state. Every $\textsf  {slot}_i$ will hold a process state of a process $i$. The \textsf  {channels} stores a copy of message channels, which keeps being updated.\relax }}{113}{figure.caption.34}}
\newlabel{fig:collate}{{7.6}{113}{The structure of a collate type object for $n$ processes. \textsf {id} denotes the identifier of the associated procedure, \textsf {tag} indicates whether the collate serves for a collective pre- or post-state. Every $\textsf {slot}_i$ will hold a process state of a process $i$. The \textsf {channels} stores a copy of message channels, which keeps being updated.\relax }{figure.caption.34}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.3}Absence Assertion Verification and Partial Order Reduction}{114}{subsection.7.3.3}}
\newlabel{sec:minimp:system:por}{{7.3.3}{114}{Absence Assertion Verification and Partial Order Reduction}{subsection.7.3.3}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {7.7}{\ignorespaces Collates in states along the on-the-fly exploration of the execution showed in Fig.\ \ref  {fig:minimp:example:collective:state}.\relax }}{115}{figure.caption.35}}
\newlabel{fig:collates:in:queue}{{7.7}{115}{Collates in states along the on-the-fly exploration of the execution showed in Fig.\^^M\ref {fig:minimp:example:collective:state}.\relax }{figure.caption.35}{}}
\citation{Palmer:2007:SDD:1273647.1273657,10.1007/978-3-540-30579-8_27,vakkalanka2008dynamic,Siegel:2005:MWM:1065944.1065957}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.4}Infinite Reachable States}{119}{subsection.7.3.4}}
\newlabel{sec:minimp:system:limitation}{{7.3.4}{119}{Infinite Reachable States}{subsection.7.3.4}{}}
\citation{Kauer:2010:MII:1860141.1860452,Sankaranarayanan04non-linearloop,McMillan:2010:LAP:2144310.2144323}
\citation{Hentschel2018}
\@writefile{toc}{\contentsline {section}{\numberline {7.4}Soundness}{120}{section.7.4}}
\newlabel{sec:minimp:system:proof}{{7.4}{120}{Soundness}{section.7.4}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.1}Soundness of The Monolithic Algorithm}{120}{subsection.7.4.1}}
\newlabel{sec:minimp:mono:proof}{{7.4.1}{120}{Soundness of The Monolithic Algorithm}{subsection.7.4.1}{}}
\newlabel{teom:mc:sound}{{7.25}{120}{}{thm.7.25}{}}
\newlabel{lema:mc:concretize}{{7.26}{121}{}{thm.7.26}{}}
\newlabel{lema:mc:prop:preserve}{{7.27}{121}{}{thm.7.27}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.4.2}Soundness of The Composite And Modular Algorithm }{122}{subsection.7.4.2}}
\newlabel{sec:minimp:modular:proof}{{7.4.2}{122}{Soundness of The Composite And Modular Algorithm}{subsection.7.4.2}{}}
\newlabel{lema:modular:2}{{7.29}{123}{}{Item.89}{}}
\newlabel{mc:delta:one:proof:a}{{{a}}{125}{Soundness of The Composite And Modular Algorithm}{Item.89}{}}
\newlabel{lema:modular:3}{{7.30}{128}{}{Item.92}{}}
\@writefile{toc}{\contentsline {part}{Part\ \numberline {III}\uppercase {$\nobreakspace  {}$Practice}}{135}{part.3}}
\citation{siegel-etal:2015:civl_sc}
\citation{Luo:2017:VMP:3127024.3127032}
\citation{barrett-etal:2011:cvc4,Z3Prover,filliatre:2013:why3}
\@writefile{toc}{\contentsline {chapter}{\numberline {8}Modeling C/MPI Programs in The CIVL Framework}{136}{chapter.8}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:mpi:model}{{8}{136}{Modeling C/MPI Programs in The CIVL Framework}{chapter.8}{}}
\@writefile{toc}{\contentsline {section}{\numberline {8.1}CIVL: The Concurrency Intermediate Verification Language}{136}{section.8.1}}
\newlabel{sec:civl}{{8.1}{136}{CIVL: The Concurrency Intermediate Verification Language}{section.8.1}{}}
\citation{iso:2011:c11}
\@writefile{lof}{\contentsline {figure}{\numberline {8.1}{\ignorespaces The layout of the CIVL framework\relax }}{137}{figure.caption.36}}
\newlabel{fig:civl:layout}{{8.1}{137}{The layout of the CIVL framework\relax }{figure.caption.36}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {8.2}{\ignorespaces A selected set of CIVL-C primitives\relax }}{138}{figure.caption.37}}
\newlabel{fig:civlc:primitives}{{8.2}{138}{A selected set of CIVL-C primitives\relax }{figure.caption.37}{}}
\@writefile{toc}{\contentsline {section}{\numberline {8.2}Modeling MPI with Transformation and Libraries}{138}{section.8.2}}
\newlabel{sec:civl:mpi-support}{{8.2}{138}{Modeling MPI with Transformation and Libraries}{section.8.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {8.3}{\ignorespaces A CIVL-C representation of a hierarchical concurrency memory model.\relax }}{139}{figure.caption.38}}
\newlabel{fig:mpi:model:civlc}{{8.3}{139}{A CIVL-C representation of a hierarchical concurrency memory model.\relax }{figure.caption.38}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {8.2.1}The MPI Library}{139}{subsection.8.2.1}}
\@writefile{lof}{\contentsline {figure}{\numberline {8.4}{\ignorespaces The definition of \texttt  {MPI\texttt  {\char `\_}{}Recv} in the MPI library in CIVL.\relax }}{140}{figure.caption.39}}
\newlabel{fig:mpi:model:MPI_Recv}{{8.4}{140}{The definition of \texttt {MPI\U {}Recv} in the MPI library in CIVL.\relax }{figure.caption.39}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {8.2.2}AST-Level Code Transformation}{142}{subsection.8.2.2}}
\@writefile{lof}{\contentsline {figure}{\numberline {8.5}{\ignorespaces The general C/MPI to CIVL-C transformation template.\relax }}{143}{figure.caption.40}}
\newlabel{fig:sec:mpi:transform}{{8.5}{143}{The general C/MPI to CIVL-C transformation template.\relax }{figure.caption.40}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {8.2.3}MPI Program Properties}{144}{subsection.8.2.3}}
\newlabel{sec:civl:mpi:quality}{{8.2.3}{144}{MPI Program Properties}{subsection.8.2.3}{}}
\@writefile{toc}{\contentsline {chapter}{\numberline {9}Verifying C/MPI Programs with Function Contracts}{146}{chapter.9}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:mpi:system}{{9}{146}{Verifying C/MPI Programs with Function Contracts}{chapter.9}{}}
\@writefile{toc}{\contentsline {section}{\numberline {9.1}Bring Function Contracts From \textsc  {MiniMP}{} To MPI}{146}{section.9.1}}
\newlabel{sec:mpi:minimp2mpi}{{9.1}{146}{Bring Function Contracts From \minimp {} To MPI}{section.9.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.1}{\ignorespaces An MPI collective-style function that requires any following statement not to send any message with tag 1 to process 0 until process 0 exits it.\relax }}{148}{figure.caption.41}}
\newlabel{fig:mpi:exmp:tag}{{9.1}{148}{An MPI collective-style function that requires any following statement not to send any message with tag 1 to process 0 until process 0 exits it.\relax }{figure.caption.41}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.2}{\ignorespaces A sequential C function with an ACSL contract.\relax }}{150}{figure.caption.42}}
\newlabel{fig:exmp:pure-acsl}{{9.2}{150}{A sequential C function with an ACSL contract.\relax }{figure.caption.42}{}}
\@writefile{toc}{\contentsline {section}{\numberline {9.2}The MPI Contract Language}{150}{section.9.2}}
\newlabel{sec:mpi:contract_language}{{9.2}{150}{The MPI Contract Language}{section.9.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.1}Syntax}{151}{subsection.9.2.1}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.3}{\ignorespaces The syntax of the behaviors of the MPI contract language.\relax }}{151}{figure.caption.43}}
\newlabel{fig:mpi:spec:syntax}{{9.3}{151}{The syntax of the behaviors of the MPI contract language.\relax }{figure.caption.43}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.4}{\ignorespaces The syntax of the expression of the MPI contract language. The \texttt  {\textit  {\leavevmode {\color  {blue}ACSL-Expr}}} stands for the expression syntax of ACSL.\relax }}{152}{figure.caption.44}}
\newlabel{fig:mpi:contract:expr_syntax}{{9.4}{152}{The syntax of the expression of the MPI contract language. The \nonterm {ACSL-Expr} stands for the expression syntax of ACSL.\relax }{figure.caption.44}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.2}Semantics}{152}{subsection.9.2.2}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.5}{\ignorespaces A collective-style MPI function \texttt  {ring} with a contract.\relax }}{153}{figure.caption.45}}
\newlabel{fig:mpi:ring:contract}{{9.5}{153}{A collective-style MPI function \texttt {ring} with a contract.\relax }{figure.caption.45}{}}
\@writefile{toc}{\contentsline {section}{\numberline {9.3}MPI Function Contract System Implementation}{155}{section.9.3}}
\newlabel{sec:mpi:impl}{{9.3}{155}{MPI Function Contract System Implementation}{section.9.3}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {9.3.1}Implementing Collates}{155}{subsection.9.3.1}}
\newlabel{sec:mpi:impl:collate}{{9.3.1}{155}{Implementing Collates}{subsection.9.3.1}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.6}{\ignorespaces CIVL-C implementation for collate and collate queue\relax }}{157}{figure.caption.46}}
\newlabel{fig:mpi:impl:data-structure}{{9.6}{157}{CIVL-C implementation for collate and collate queue\relax }{figure.caption.46}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.7}{\ignorespaces A CIVL state of a CIVL-C program transformed from an general MPI program, which contains a function \texttt  {f}. The boxes labeled by \textbf  {d0, d1, ...} are dyscopes. Arrows between dyscopes denote the ``parent-of'' relation. Boxes under ``p0, p1, p2'' are call stack entries. Dashed arrows mark the referred dyscope of every call stack entry.\relax }}{159}{figure.caption.47}}
\newlabel{fig:civl:state}{{9.7}{159}{A CIVL state of a CIVL-C program transformed from an general MPI program, which contains a function \texttt {f}. The boxes labeled by \textbf {d0, d1, ...} are dyscopes. Arrows between dyscopes denote the ``parent-of'' relation. Boxes under ``p0, p1, p2'' are call stack entries. Dashed arrows mark the referred dyscope of every call stack entry.\relax }{figure.caption.47}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.8}{\ignorespaces Merging a snapshot to a state. The snapshot (on the right) was taken from the state in Fig.\ \ref  {fig:civl:state} for process p1.\relax }}{160}{figure.caption.48}}
\newlabel{fig:state:merge}{{9.8}{160}{Merging a snapshot to a state. The snapshot (on the right) was taken from the state in Fig.\ \ref {fig:civl:state} for process p1.\relax }{figure.caption.48}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {9.3.2}Implementing Absence Assertions}{161}{subsection.9.3.2}}
\newlabel{sec:mpi:impl:absence}{{9.3.2}{161}{Implementing Absence Assertions}{subsection.9.3.2}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {9.3.3}Transformation}{162}{subsection.9.3.3}}
\newlabel{sec:mpi:impl:transform}{{9.3.3}{162}{Transformation}{subsection.9.3.3}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.9}{\ignorespaces The simplified code of the CIVL-C function that will be called every time a send operation was performed by a process in order to check for the free of \textbf  {PGV}.\relax }}{163}{figure.caption.49}}
\newlabel{fig:mpi:imple:check:upsilon}{{9.9}{163}{The simplified code of the CIVL-C function that will be called every time a send operation was performed by a process in order to check for the free of \textbf {PGV}.\relax }{figure.caption.49}{}}
\citation{java8}
\@writefile{lof}{\contentsline {figure}{\numberline {9.10}{\ignorespaces Transformation template for generating \texttt  {f\texttt  {\char `\_}{}driver} from a function \texttt  {f} with its contract. The upper shows the original annotated function \texttt  {f} and the lower shows the generated \texttt  {f\texttt  {\char `\_}{}driver}.\relax }}{167}{figure.caption.50}}
\newlabel{fig:mpi:impl:transform:driver}{{9.10}{167}{Transformation template for generating \texttt {f\U {}driver} from a function \texttt {f} with its contract. The upper shows the original annotated function \texttt {f} and the lower shows the generated \texttt {f\U {}driver}.\relax }{figure.caption.50}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {9.11}{\ignorespaces The transformation template for summarizing \texttt  {f} with respect to its contract.\relax }}{169}{figure.caption.51}}
\newlabel{fig:mpi:impl:transform:callee}{{9.11}{169}{The transformation template for summarizing \texttt {f} with respect to its contract.\relax }{figure.caption.51}{}}
\citation{Thakur:2005:OCC:2747766.2747771}
\citation{jesper2019optimal,KANG2019220}
\@writefile{toc}{\contentsline {chapter}{\numberline {10}Evaluation}{170}{chapter.10}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:mpi:eval}{{10}{170}{Evaluation}{chapter.10}{}}
\@writefile{toc}{\contentsline {section}{\numberline {10.1}Running Examples}{170}{section.10.1}}
\newlabel{chp:eval:examples}{{10.1}{170}{Running Examples}{section.10.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {10.1.1}Allgather Implementations}{171}{subsection.10.1.1}}
\newlabel{sec:mpi:eval:allgather}{{10.1.1}{171}{Allgather Implementations}{subsection.10.1.1}{}}
\citation{Ruefenacht:2017:GRD:3163938.3164013}
\@writefile{lof}{\contentsline {figure}{\numberline {10.1}{\ignorespaces Annotating function contracts for all the collective-style functions used by CIVL's implementation of \texttt  {MPI\texttt  {\char `\_}{}Allreduce}.\relax }}{173}{figure.caption.52}}
\newlabel{fig:mpi:eval:allgather}{{10.1}{173}{Annotating function contracts for all the collective-style functions used by CIVL's implementation of \texttt {MPI\U {}Allreduce}.\relax }{figure.caption.52}{}}
\citation{falgout:2002:hypre}
\@writefile{toc}{\contentsline {subsection}{\numberline {10.1.2}Parallel Vector Product}{174}{subsection.10.1.2}}
\newlabel{sec:mpi:eval:dotprod}{{10.1.2}{174}{Parallel Vector Product}{subsection.10.1.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {10.2}{\ignorespaces An \texttt  {MPI\texttt  {\char `\_}{}Allreduce} implementation based on the recursive doubling algorithm.\relax }}{175}{figure.caption.53}}
\newlabel{fig:mpi:eval:recursive-double}{{10.2}{175}{An \texttt {MPI\U {}Allreduce} implementation based on the recursive doubling algorithm.\relax }{figure.caption.53}{}}
\citation{10.1007/978-3-030-03421-4_12}
\@writefile{lof}{\contentsline {figure}{\numberline {10.3}{\ignorespaces The data structures that are used in Fig.\ \ref  {fig:mpi:dotprod}. Insignificant fields are omitted.\relax }}{176}{figure.caption.54}}
\newlabel{fig:mpi:dotprod:structures}{{10.3}{176}{The data structures that are used in Fig.\^^M\ref {fig:mpi:dotprod}. Insignificant fields are omitted.\relax }{figure.caption.54}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {10.4}{\ignorespaces A function that computes vector product in parallel using MPI.\relax }}{177}{figure.caption.55}}
\newlabel{fig:mpi:dotprod}{{10.4}{177}{A function that computes vector product in parallel using MPI.\relax }{figure.caption.55}{}}
\@writefile{toc}{\contentsline {section}{\numberline {10.2}Experiment}{178}{section.10.2}}
\newlabel{chp:eval:results}{{10.2}{178}{Experiment}{section.10.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {10.5}{\ignorespaces The definition of the \texttt  {matmat} function that collectively performs matrix multiplication.\relax }}{181}{figure.caption.56}}
\newlabel{fig:eval:matmat}{{10.5}{181}{The definition of the \texttt {matmat} function that collectively performs matrix multiplication.\relax }{figure.caption.56}{}}
\citation{Ruefenacht:2017:GRD:3163938.3164013}
\citation{Bernaschi:2002:EIR:1895489.1895529}
\citation{falgout:2002:hypre}
\@writefile{lof}{\contentsline {figure}{\numberline {10.6}{\ignorespaces Function contract of the function in the \texttt  {OddEvenSort} example.\relax }}{182}{figure.caption.57}}
\newlabel{fig:eval:oddEvenSort}{{10.6}{182}{Function contract of the function in the \texttt {OddEvenSort} example.\relax }{figure.caption.57}{}}
\@writefile{lot}{\contentsline {table}{\numberline {10.1}{\ignorespaces The experimental results of verifying CIVL's implementations of the MPI collective functions with respect to state-requirements and -guarantees.\relax }}{183}{table.caption.58}}
\newlabel{tab:experimental:result:part:I-1}{{10.1}{183}{The experimental results of verifying CIVL's implementations of the MPI collective functions with respect to state-requirements and -guarantees.\relax }{table.caption.58}{}}
\@writefile{lot}{\contentsline {table}{\numberline {10.2}{\ignorespaces The experimental results of verifying MPI collective-style functions with respect to state-requirements and -guarantees. The experiments are under an assumption that no interference can happen.\relax }}{184}{table.caption.59}}
\newlabel{tab:experimental:result:part:I-2}{{10.2}{184}{The experimental results of verifying MPI collective-style functions with respect to state-requirements and -guarantees. The experiments are under an assumption that no interference can happen.\relax }{table.caption.59}{}}
\@writefile{lot}{\contentsline {table}{\numberline {10.3}{\ignorespaces The experimental results of verifying full validity of MPI collective-style functions.\relax }}{185}{table.caption.60}}
\newlabel{tab:experimental:result:part:II}{{10.3}{185}{The experimental results of verifying full validity of MPI collective-style functions.\relax }{table.caption.60}{}}
\@writefile{toc}{\contentsline {chapter}{\numberline {11}Summary and Future Work}{187}{chapter.11}}
\@writefile{loa}{\addvspace {10\p@ }}
\newlabel{chp:conclusion}{{11}{187}{Summary and Future Work}{chapter.11}{}}
\@writefile{toc}{\contentsline {section}{\numberline {11.1}Dissertation Summary}{187}{section.11.1}}
\citation{10.1007/978-3-642-27940-9_27}
\@writefile{toc}{\contentsline {section}{\numberline {11.2}Future Work}{189}{section.11.2}}
\citation{cohen-etal:2009:vcc,blom:2017:vercors,beckert:2007:KeY,amani:2017:complex}
\citation{luo2018towards}
\citation{luo2018towards}
\bibstyle{abbrv}
\bibdata{bib}
\bibcite{ACSL:Reference}{1}
\bibcite{ada2012}{2}
\bibcite{spark}{3}
\bibcite{amani:2017:complex}{4}
\bibcite{araujo:2011:enabling}{5}
\bibcite{armstrong:2013:programming}{6}
\bibcite{Ashcroft:1975:PAP:1739967.1740302}{7}
\bibcite{ball:2010:towards}{8}
\bibcite{Barnes:2012:SPA}{9}
\bibcite{barnett:2006:boogie}{10}
\@writefile{toc}{\contentsline {chapter}{\uppercase {Bibliography}}{191}{chapter*.61}}
\bibcite{barnett:2005:specsharp}{11}
\bibcite{barrett-etal:2011:cvc4}{12}
\bibcite{beckert:2007:KeY}{13}
\bibcite{bergstra2001handbook}{14}
\bibcite{Bernaschi:2002:EIR:1895489.1895529}{15}
\bibcite{bernholdt-etal:2018:mpi_exascale}{16}
\bibcite{biere:2003:bounded}{17}
\bibcite{blom:2017:vercors}{18}
\bibcite{board:1993:ieee}{19}
\bibcite{Bronevetsky:2009:CSD:1545006.1545049}{20}
\bibcite{christakis:2011:detection}{21}
\bibcite{clangstaticanalyzer}{22}
\bibcite{clarke:2000:modelchecking}{23}
\bibcite{clarke:1976:symbolically}{24}
\bibcite{cohen-etal:2009:vcc}{25}
\bibcite{alt-ergo}{26}
\bibcite{correctness:2017:proceedings}{27}
\bibcite{correctness:2018:proceedings}{28}
\bibcite{Cranen:2013:OMT:2450387.2450410}{29}
\bibcite{cuoq2012framac}{30}
\bibcite{cuoq:2011:wp}{31}
\bibcite{dannenberg:1982:formal}{32}
\bibcite{Z3Prover}{33}
\bibcite{drake:2005:overview}{34}
\bibcite{Droste:2015:MSA:2833157.2833159}{35}
\bibcite{dwyer:1999:patterns}{36}
\bibcite{falgout:2002:hypre}{37}
\bibcite{filliatre:2013:why3}{38}
\bibcite{Floyd1993}{39}
\bibcite{Forejt:2017:PPA:3133234.3095075}{40}
\bibcite{godefroid:1993:refining}{41}
\bibcite{gopalakrishnan-etal:2017:correctness}{42}
\bibcite{gordon:1989:mechanizing}{43}
\bibcite{Gosling:2014:JLS:2636997}{44}
\bibcite{hatton:1997:T_Experiments}{45}
\bibcite{hatton:2012:defects}{46}
\bibcite{hatton-roberts:1994:accurate}{47}
\bibcite{Hentschel2018}{48}
\bibcite{Hilbrich:2012:MRE:2388996.2389037}{49}
\bibcite{hoare:1969:axiomatic}{50}
\bibcite{Hoare:1985:CSP:3921}{51}
\bibcite{holzmann1997spin}{52}
\bibcite{huchant2019multivalued}{53}
\bibcite{iso:2011:c11}{54}
\bibcite{Jackson:2006:SAL}{55}
\bibcite{Jacobs:2010:QTV:1947873.1947902}{56}
\bibcite{java8}{57}
\bibcite{johansen:2017:earthquake}{58}
\bibcite{KANG2019220}{59}
\bibcite{10.1007/BFb0013032}{60}
\bibcite{Kauer:2010:MII:1860141.1860452}{61}
\bibcite{khanna2018dynamic}{62}
\bibcite{king:1976:symbolic}{63}
\bibcite{Kleymann:1999:HLA:2769784.2769811}{64}
\bibcite{kovacs:2013:firstorder}{65}
\bibcite{krammer2004marmot}{66}
\bibcite{krenn:2009:test}{67}
\bibcite{kroening:2014:cbmc}{68}
\bibcite{lahiri2012security}{69}
\bibcite{lamport:1980:hoare}{70}
\bibcite{leavens:1999:jml}{71}
\bibcite{leino:2010:dafny}{72}
\bibcite{leino:2009:verification}{73}
\bibcite{leino:1999:checkingjava}{74}
\bibcite{lipton:reduction}{75}
\bibcite{Lopez:2015:PVM:2814270.2814302}{76}
\bibcite{10.1007/978-3-030-03421-4_12}{77}
\bibcite{luo2018towards}{78}
\bibcite{Luo:2017:VMP:3127024.3127032}{79}
\bibcite{Manna:1984:APP:2731.2734}{80}
\bibcite{mathuriya:2017:embracingquantum}{81}
\bibcite{mcmillan:1993:symbolic}{82}
\bibcite{McMillan:2010:LAP:2144310.2144323}{83}
\bibcite{merali:2010:error}{84}
\bibcite{mpi-forum:2015:mpi31}{85}
\bibcite{Meyer:1988:eiffel}{86}
\bibcite{Meyer:1992:ADC}{87}
\bibcite{Newton1975}{88}
\bibcite{oortwijn2016future}{89}
\bibcite{Owicki1976}{90}
\bibcite{Owicki:1982:PLP:357172.357178}{91}
\bibcite{Palmer:2007:SDD:1273647.1273657}{92}
\bibcite{rebelo:2014:aspectjml}{93}
\bibcite{reynolds2002separation}{94}
\bibcite{romano-etal:2015:openmc}{95}
\bibcite{Ruefenacht:2017:GRD:3163938.3164013}{96}
\bibcite{Sankaranarayanan04non-linearloop}{97}
\bibcite{10.1007/978-3-540-30579-8_27}{98}
\bibcite{siegel2007verifying}{99}
\bibcite{Siegel:2005:MWM:1065944.1065957}{100}
\bibcite{siegel-etal:2015:civl_sc}{101}
\bibcite{siegel2011tass}{102}
\bibcite{10.1007/978-3-642-27940-9_27}{103}
\bibcite{Stark:1985:PTR:646823.706907}{104}
\bibcite{Strout:2006:DAM:1156433.1157634}{105}
\bibcite{Takaoka:1994:PPV:326619.326811}{106}
\bibcite{Thakur:2005:OCC:2747766.2747771}{107}
\bibcite{jesper2019optimal}{108}
\bibcite{vakkalanka2008dynamic}{109}
\bibcite{valiev:2010:nwchem}{110}
\bibcite{Valmari1992}{111}
\bibcite{vandevoorde:1994:specializedprocedures}{112}
\bibcite{Vo:2010:SDD:1884643.1884681}{113}
\bibcite{yang-etal:2017:amg}{114}
\bibcite{ye:2018:detecting}{115}
\bibcite{Yu:2018:CSE:3183440.3190336}{116}
\bibcite{zheng-etal:2016:civl_tacas}{117}
\bibcite{zheng-etal:2015:civl_ase}{118}
\bibcite{zheng:2008:test}{119}