%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Thin Sectioned Essay
% LaTeX Template
% Version 1.0 (3/8/13)
%
% This template has been downloaded from:
% http://www.LaTeXTemplates.com
%
% Original Author:
% Nicolas Diaz (nsdiaz@uc.cl) with extensive modifications by:
% Vel (vel@latextemplates.com)
%
% License:
% CC BY-NC-SA 3.0 (http://creativecommons.org/licenses/by-nc-sa/3.0/)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%----------------------------------------------------------------------------------------
%	PACKAGES AND OTHER DOCUMENT CONFIGURATIONS
%----------------------------------------------------------------------------------------

\documentclass[10pt]{report} % Font size (can be 10pt, 11pt or 12pt) and paper size (remove a4paper for US letter paper)
\usepackage[dvipdfmx]{graphicx} % Required for including pictures
\usepackage{cite}
\usepackage{float}
\usepackage{url}
\usepackage{color}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{subcaption}
\usepackage{comment}
\usepackage{hyperref}

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

\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{exmp}[thm]{Example} % same for example numbers

\input{preambular}

%----------------------------------------------------------------------------------------
%	TITLE
%----------------------------------------------------------------------------------------

\title{\textbf{Verification and Specification for Message-Passing Programs}\\ % Title
} % Subtitle

\author{\textsc{Ziqing Luo} % Author
\\{\textit{University of Delaware}}} % Institution

\date{\today} % Date

%----------------------------------------------------------------------------------------

\begin{document}

\maketitle % Print the title section

%----------------------------------------------------------------------------------------
%	ABSTRACT AND KEYWORDS
%----------------------------------------------------------------------------------------

%\renewcommand{\abstractname}{Summary} % Uncomment to change the name of the abstract to something else
\vspace{30pt} % Some vertical space between the abstract and first section

%----------------------------------------------------------------------------------------
%	ESSAY BODY
%----------------------------------------------------------------------------------------
\tableofcontents

\chapter{The MiniMP Programming Language} \ref{chp:minimp}
\input{lan_semantics}

\chapter{Verifying MiniMP Programs with Function Contracts}
\input{lan_spec}
\input{lan_spec_rules}
\input{lan_spec_symExe}
\input{lan_spec_symExeModular}
\input{lan_spec_contract}
\input{lan_verification}

\chapter{Verifying C/MPI Programs using CIVL}
\input{mpi_chp/intro}
\input{mpi_chp/model}

\chapter{Verifying C/MPI Programs with Function Contracts}
\input{mpi_chp/minimp2mpi}
\input{mpi_chp/lang}
\input{mpi_chp/impl}


%\input{examples}

%----------------------------------------------------------------------------------------
%	BIBLIOGRAPHY
%----------------------------------------------------------------------------------------

\bibliographystyle{abbrv} \bibliography{../../ziqing}
%----------------------------------------------------------------------------------------

\end{document}