% This file (dissertation-main.tex) is the main file for a dissertation.
\documentclass {udthesis}
% preamble

% Include graphicx package for the example image used
% Use LaTeX->PDF if including graphics such as .jpg, .png or .pdf.
% Use LaTeX->PS->PDF if including graphics such as .ps or .eps
% Best practice to not specify the file extension for included images,
% so when LaTeX is building it will look for the appropriate image type.
\usepackage{graphicx}
\usepackage{url}
\usepackage{color}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{comment}
\usepackage{subcaption}
\usepackage{hyperref}
\usepackage{multirow}
\usepackage{cite}
\usepackage{tikz}
\usepackage{lmodern}
\usepackage[]{algorithm2e}
%\usepackage[toc]{glossaries} 
\graphicspath{{../images}}

\input{preambular}
%\input{myglossaries}
%\makeglossaries                                   % activate glossaries-package

\theoremstyle{plain}
\newtheorem{thm}{Theorem}[chapter]

\theoremstyle{definition}
\newtheorem{defn}[thm]{Definition} % definition numbers are dependent on theorem numbers
\newtheorem{teom}[thm]{Theorem} % definition numbers are dependent on theorem numbers
\newtheorem{lema}[thm]{Lemma} % definition numbers are dependent on theorem numbers
\newtheorem{limt}[thm]{Limitation} % same for limitation numbers
\newtheorem{rest}[thm]{Restriction} % same for restriction numbers
\newtheorem{exmp}[thm]{Example} % same for example numbers
\newtheorem{coro}[thm]{Corollary} % same for example numbers
               
\begin{document}
\include{template}    % This file (dissertation-tap.tex) contains the Title
% and Approval Page information for a dissertation.

% \tableofcontents

\part{$~$Preliminaries}

\chapter{Introduction} \label{chp:intro}
\input{01_intro}
%% Message-Passing
%% MODEL-CHECING & SYMBOLIC EXE
%% HOARE LOGIC
%% ACSL
\chapter{Background \& Related Work} \label{chp:background-related}
\input{02_background}
%\input{relatedwork}

\chapter{Notation} \label{chp:notation}
\input{03_notation}

\part{$~$Theory} \label{part:2}

\chapter{The MiniMP Programming Language} \label{chp:minimp}
\input{04_lan_semantics}

\chapter{The Specification Language for MiniMP} \label{chp:minimp:spec}
\input{05_lan_spec}

\chapter{A Inference System for MiniMP} \label{chp:minimp:rules}
\input{06_rules}

\chapter{A Verification System for MiniMP} \label{chp:minimp:system}
\input{07_1_symExe}
\input{07_2_modularSymExe}
\input{07_3_contract}
\input{07_4_system}
\input{07_5_sound} 

\part{$~$Practice}

\chapter{Modeling C/MPI Programs in The CIVL Framework} \label{chp:mpi:model}
\input{08_civl/1_intro}
\input{08_civl/2_model}

\chapter{Verifying C/MPI Programs with Function Contracts} \label{chp:mpi:system}
\input{09_mpi_spec/3_minimp2mpi}
\input{09_mpi_spec/4_lang}
\input{09_mpi_spec/5_impl}

\chapter{Evaluation} \label{chp:mpi:eval}
\input{10_eval}

\chapter{Summary and Future Work} \label{chp:conclusion}
\input{11_conclusion}

\bibliographystyle{abbrv} \bibliography{bib}
%\printglossaries
\end{document}