\relax 
\citation{cobleigh01}
\newlabel{introduction}{{}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {I}Introduction}{2}}
\citation{owen07}
\citation{owen02a}
\citation{menzies02,owen02c,owen02b}
\citation{owen03a}
\citation{holzmann03}
\citation{mcmillan00}
\citation{owen03b}
\citation{owen06}
\citation{heitmeyer05}
\citation{huth00}
\citation{holzmann97,clarke99,cimatti00}
\citation{havelund00,gluck02,holzmann04}
\citation{ball01}
\citation{clarke99}
\citation{clarke99}
\citation{mcmillan00}
\citation{cimatti00}
\newlabel{related}{{I}{5}}
\@writefile{toc}{\contentsline {section}{\numberline {II}Related Work}{5}}
\@writefile{toc}{\contentsline {subsection}{\numberline {II-A}Model Checking}{5}}
\newlabel{model-checking}{{II-A}{5}}
\newlabel{mctest}{{II-A}{5}}
\citation{holzmann97}
\citation{clarke99,holzmann97}
\citation{holzmann90,holzmann97,holzmann03}
\citation{holzmann03}
\citation{holzmann03}
\citation{holzmann87}
\citation{owen02a}
\citation{biere99}
\citation{cobleigh01,groce02}
\citation{dong03}
\citation{gargantini99,heimdahl03}
\citation{savage97,godefroid97,sims01,groce02}
\citation{corbett96,cobleigh01,groce02}
\citation{bharadwaj99,cobleigh01}
\citation{west89}
\citation{west89}
\@writefile{toc}{\contentsline {subsection}{\numberline {II-B}Random Search Applied to Formal Models}{7}}
\newlabel{west-random}{{II-B}{7}}
\citation{chockler06}
\citation{mcmillan00}
\citation{cimatti00}
\newlabel{motivation}{{II-B}{8}}
\@writefile{toc}{\contentsline {section}{\numberline {III}Motivating Examples}{8}}
\newlabel{examples}{{III}{8}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Inconsistent outputs from Cadence SMV (top) and NuSMV (bottom) running on the same fault-seeded specification.}}{9}}
\newlabel{f:smv_output}{{1}{9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {III-A}Inconsistent Results from Two Symbolic Model Checkers}{9}}
\newlabel{utpb527}{{III-A}{9}}
\citation{holzmann03}
\citation{owen06}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Output from SPIN running on a model generated from the same fault-seeded specification used to generate the models for which Cadence SMV and NuSMV outputs are shown in figure 1\hbox {}.}}{10}}
\newlabel{f:spin_output}{{2}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {III-B}Inconsistent Results from Model Checking and Random Search}{10}}
\newlabel{utpb23}{{III-B}{10}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Inconsistent outputs from SPIN (top) and Lurch (bottom) running on input models generated from the same fault-seeded specification.}}{11}}
\newlabel{f:splu_output}{{3}{11}}
\citation{bharadwaj00}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Simulator log produced by stepping through execution trace output by Lurch.}}{12}}
\newlabel{f:sim_output}{{4}{12}}
\@writefile{toc}{\contentsline {subsection}{\numberline {III-C}Inconsistent Results from an Invariant Checker and a Model Checker}{12}}
\newlabel{sasp}{{III-C}{12}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces Inconsistent outputs from Salsa (top) and SPIN (bottom) running on input models generated from the same fault-seeded specification.}}{13}}
\newlabel{f:sasp-output}{{5}{13}}
\citation{heitmeyer05}
\newlabel{dsn08-background}{{III-C}{14}}
\@writefile{toc}{\contentsline {section}{\numberline {IV}Modeling and Verification Framework}{14}}
\newlabel{framework}{{IV}{14}}
\@writefile{toc}{\contentsline {subsection}{\numberline {IV-A}The SCR Toolset}{14}}
\citation{archer02}
\citation{mcmillan00}
\citation{cimatti02}
\@writefile{toc}{\contentsline {subsection}{\numberline {IV-B}The Cadence SMV and NuSMV Symbolic Model Checkers}{15}}
\citation{holzmann03}
\citation{bharadwaj00,sims01}
\@writefile{toc}{\contentsline {subsection}{\numberline {IV-C}The SPIN Explicit-State Model Checker}{16}}
\@writefile{toc}{\contentsline {subsection}{\numberline {IV-D}The Salsa Invariant Checker}{16}}
\citation{owen03a}
\citation{menzies02}
\citation{owen06}
\citation{owen07}
\@writefile{toc}{\contentsline {subsection}{\numberline {IV-E}The Lurch Random Search Tool}{17}}
\newlabel{case-study}{{IV-E}{17}}
\@writefile{toc}{\contentsline {section}{\numberline {V}Case Study}{17}}
\citation{nsa03}
\citation{widmaier00}
\citation{desovski06}
\@writefile{toc}{\contentsline {subsection}{\numberline {V-A}PACS SCR Specification}{18}}
\newlabel{pacs}{{V-A}{18}}
\citation{owen07}
\@writefile{lof}{\contentsline {figure}{\numberline {6}{\ignorespaces PACS mode finite-state machine.}}{19}}
\newlabel{f:pacs2}{{6}{19}}
\citation{offutt96}
\citation{offutt96}
\citation{owen07}
\@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces Mutation operators used to generate fault-seeded versions of the PACS SCR specification.}}{20}}
\newlabel{t:operators}{{7}{20}}
\@writefile{toc}{\contentsline {subsection}{\numberline {V-B}Generating Fault-Seeded Versions of the PACS SCR Specification}{20}}
\newlabel{seeding}{{V-B}{20}}
\citation{andrews06}
\@writefile{toc}{\contentsline {subsection}{\numberline {V-C}Experiments}{21}}
\newlabel{experiments}{{V-C}{21}}
\@writefile{lof}{\contentsline {figure}{\numberline {8}{\ignorespaces Lurch results on fault-seeded PACS specifications: number of times violations detected vs.\nobreakspace  {}search runs, number of specifications in parentheses. For example, ``10 / 10 | (175)'' means that, for 175 of the fault-seeded specifications, Lurch found violations in 10 of 10 runs on that specification. }}{23}}
\newlabel{t:lurch-runs}{{8}{23}}
\@writefile{lof}{\contentsline {figure}{\numberline {9}{\ignorespaces Summary of verification results for all tools except Salsa---sets of fault-seeded specifications for which each tool detected property violations.}}{25}}
\newlabel{f:venn}{{9}{25}}
\@writefile{lof}{\contentsline {figure}{\numberline {10}{\ignorespaces Specifications plotted to show maximum and minimum time requirements for any tool.}}{26}}
\newlabel{f:min-max-time}{{10}{26}}
\newlabel{discussion}{{V-C}{26}}
\@writefile{toc}{\contentsline {section}{\numberline {VI}Discussion}{26}}
\@writefile{toc}{\contentsline {subsection}{\numberline {VI-A}Performance Variations Between Verification Strategies}{26}}
\newlabel{variations}{{VI-A}{26}}
\@writefile{lof}{\contentsline {figure}{\numberline {11}{\ignorespaces Specifications plotted to show maximum and minimum memory requirements for any tool.}}{27}}
\newlabel{f:min-max-memory}{{11}{27}}
\@writefile{toc}{\contentsline {subsection}{\numberline {VI-B}Tool-Specific Lessons Learned}{28}}
\@writefile{lof}{\contentsline {figure}{\numberline {12}{\ignorespaces Combined strategy exploiting complementary variations in performance and accuracy. }}{30}}
\newlabel{f:combo2-flow-chart}{{12}{30}}
\@writefile{toc}{\contentsline {subsection}{\numberline {VI-C}A General Multiple-Tool Verification Strategy}{30}}
\newlabel{conclusion}{{VI-C}{31}}
\@writefile{toc}{\contentsline {section}{\numberline {VII}Conclusion}{31}}
\@writefile{lof}{\contentsline {figure}{\numberline {13}{\ignorespaces A conceptual model of the challenges involved in using automatic verification tools.}}{33}}
\newlabel{f:bojan-diagram}{{13}{33}}
\bibstyle{IEEEtran.bst}
\bibdata{phd}
\bibcite{cobleigh01}{1}
\bibcite{owen07}{2}
\bibcite{owen02a}{3}
\bibcite{menzies02}{4}
\bibcite{owen02c}{5}
\bibcite{owen02b}{6}
\bibcite{owen03a}{7}
\bibcite{holzmann03}{8}
\bibcite{mcmillan00}{9}
\bibcite{owen03b}{10}
\@writefile{toc}{\contentsline {section}{References}{35}}
\bibcite{owen06}{11}
\bibcite{heitmeyer05}{12}
\bibcite{huth00}{13}
\bibcite{holzmann97}{14}
\bibcite{clarke99}{15}
\bibcite{cimatti00}{16}
\bibcite{havelund00}{17}
\bibcite{gluck02}{18}
\bibcite{holzmann04}{19}
\bibcite{ball01}{20}
\bibcite{holzmann90}{21}
\bibcite{holzmann87}{22}
\bibcite{biere99}{23}
\bibcite{groce02}{24}
\bibcite{dong03}{25}
\bibcite{gargantini99}{26}
\bibcite{heimdahl03}{27}
\bibcite{savage97}{28}
\bibcite{godefroid97}{29}
\bibcite{sims01}{30}
\bibcite{corbett96}{31}
\bibcite{bharadwaj99}{32}
\bibcite{west89}{33}
\bibcite{chockler06}{34}
\bibcite{bharadwaj00}{35}
\bibcite{archer02}{36}
\bibcite{cimatti02}{37}
\bibcite{nsa03}{38}
\bibcite{widmaier00}{39}
\bibcite{desovski06}{40}
\bibcite{offutt96}{41}
\bibcite{andrews06}{42}