%\usepackage{amsmath,amssymb,stmaryrd} \usepackage{graphicx} \usepackage{url} \usefonttheme[onlymath]{serif} \setbeamersize{text margin left=2mm, text margin right=1mm, % sidebar width left=0mm, sidebar width right=3mm} \graphicspath{{../images/}} \author{Stephen F.\ Siegel} \institute{Department of Computer and Information Sciences\\University of Delaware} %\newenvironment{pic}[4]{\begin{pgfpictureboxed}{#1}{#2}{#3}{#4}}{\end{pgfpictureboxed}} \newenvironment{pic}[4]{\begin{pgfpicture}{#1}{#2}{#3}{#4}}{\end{pgfpicture}} \newcommand{\myurl}[1]{\textcolor{blue}{\url{#1}}} \newcommand{\foot}[1]{% \usefoottemplate{\hspace{0mm}\raisebox{1mm}[0mm][0mm]{% \makebox[0pt][l]{\tiny \color{blue!50} S.F.\ Siegel $\diamond$ University of Delaware $\diamond$ #1 \hspace{1mm} {\color{black!100}\insertframenumber}}}}} \newcommand{\code}[1]{\textcolor{blue}{\texttt{#1}}} \newcommand{\U}{{\ttfamily\symbol{'137}}} \newcommand{\lb}{\texttt{\char`\{}} \newcommand{\rb}{\texttt{\char`\}}} \newcommand{\bs}{\texttt{\char`\\}} \newcommand{\ra}{\rightarrow} \renewcommand{\implies}{\Rightarrow} \renewcommand{\iff}{\Leftrightarrow} %\renewcommand{\emptyset}{\varphi} \newcommand{\Z}{\mathbb{Z}} \newcommand{\N}{\mathbb{N}} \newcommand{\R}{\mathbb{R}} \newcommand{\spin}{\textsc{Spin}} \newcommand{\mpispin}{\textsc{Mpi-Spin}} \newcommand{\x}{\mathbf{x}} \newcommand{\y}{\mathbf{y}} \newcommand{\mat}[4]{\bigl(\begin{smallmatrix}#1\\#3\end{smallmatrix}\bigr)} \newcommand{\model}{\mathcal{M}} \newcommand{\vocab}{\mathcal{V}} \newcommand{\vars}{\mathcal{X}} \newcommand{\valof}[1]{\llbracket #1 \rrbracket} \newcommand{\valofma}[1]{\valof{#1}_{\model}(\alpha)} \newcommand{\true}{\textbf{T}} \newcommand{\false}{\textbf{F}} \newcommand{\satisfies}{\models} \newcommand{\infers}{\vdash} \newcommand{\sep}{\hspace{3mm}} \newcommand{\Vars}{\textsf{Vars}} \newcommand{\FV}{\textsf{FV}} \newcommand{\fmap}[1]{\lceil#1\rceil} \newcommand{\myForm}{\textbf{Form}} \newcommand{\Prop}{\textbf{Prop}} \newcommand{\PL}{\textsf{PL}} \newcommand{\FOL}{\textsf{FOL}} \newcommand{\BV}{\textsf{BV}} \newtheorem{proposition}{Proposition} \newcommand{\attribute}[1]{\par\begin{flushright}\tiny\textcolor{gray}{---\ #1}\end{flushright}\par} \newcommand{\pSymbs}{\textsf{pSymbs}} \newcommand{\NPL}{\mathcal{N}_{\textsf{PL}}} \newcommand{\Herb}{\mathcal{H}} \newcommand{\DHerb}{D_\Herb} \newcommand{\IH}{I_\Herb} \newcommand{\sorts}{\mathcal{S}} \newcommand{\bool}{\textsf{bool}} \newcommand{\theory}{\mathcal{T}} \newcommand{\aread}{\textit{read}} \newcommand{\awrite}{\textit{write}} \newcommand{\sarrow}{\leadsto} \newenvironment{hoare}{% \begin{displaymath}% \renewcommand{\arraystretch}{4}% \begin{array}[t]{r@{.\hspace{4mm}}l@{\hspace{5mm}}l}% }{% \end{array}% \end{displaymath}% } \newcommand{\bigtrip}[3]{% {% \renewcommand{\arraystretch}{1}% \begin{array}[c]{l}% {\color{blue}\{#1\}}\\\hspace{5mm}#2\\{\color{blue}\{#3\}}% \end{array}% }% } \newcommand{\ttrip}[3]{% {% \renewcommand{\arraystretch}{1}% \begin{array}[c]{l}% {\color{blue}[#1]}\\\hspace{5mm}#2\\{\color{blue}[#3]}% \end{array}% }% } \newcommand{\trip}[3]{% {\color{blue}\{#1\}}\: #2\: {\color{blue}\{#3\}}% } \newcommand{\assign}{\textit{assign}} \newcommand{\seq}{\textit{seq}} \newcommand{\conseq}{\textit{conseq}} \newcommand{\pwhile}{\textbf{while}} \newcommand{\pdo}{\textbf{do}} \newcommand{\rwhile}{\textit{while}} \newcommand{\pskip}{\textbf{skip}} \newcommand{\pif}{\textbf{if}} \newcommand{\pelse}{\textbf{else}} \newcommand{\pthen}{\textbf{then}} \newcommand{\Ax}{\text{Ax}} \newcommand{\I}{\text{I}} \newcommand{\E}{\text{E}} \newcommand{\W}{\text{W}} \newcommand{\RAA}{\text{RAA}} \newcommand{\B}{\mathbb{B}} \newcommand{\opstyle}[1]{\textsf{\textcolor{blue}{#1}}} \newcommand{\TS}{\opstyle{TS}} \newcommand{\TT}{\opstyle{TT}} \newcommand{\LT}{\opstyle{LT}} \newcommand{\LL}{\opstyle{LL}} \newcommand{\TL}{\opstyle{TL}} \newcommand{\TE}{\opstyle{TE}} \newcommand{\ET}{\opstyle{ET}} \newcommand{\Act}{\opstyle{Act}} \newcommand{\AP}{\opstyle{AP}} \newcommand{\ul}{\opstyle{ul}} \newcommand{\ur}{\opstyle{ur}} \newcommand{\dl}{\opstyle{dl}} \newcommand{\dr}{\opstyle{dr}} \newcommand{\defeq}{\stackrel{\text{def}}{=}} \newcommand{\Post}{\opstyle{Post}} \newcommand{\Pre}{\opstyle{Pre}} \newcommand{\Reach}{\opstyle{Reach}} \newcommand{\dom}{\opstyle{dom}} %\newcommand{\true}{\textit{true}} %\newcommand{\false}{\textit{false}} \newcommand{\Eval}{\opstyle{Eval}} \newcommand{\Cond}{\opstyle{Cond}} \newcommand{\Loc}{\opstyle{Loc}} \newcommand{\Effect}{\opstyle{Effect}} \newcommand*{\hra}{\ensuremath{\lhook\joinrel\relbar\joinrel\rightarrow}} % use \xhookrightarrow{g:\alpha} instead \newcommand{\xra}[1]{\xrightarrow{#1}} \newcommand{\xhra}[1]{\xhookrightarrow{#1}} \newcommand{\PG}{\opstyle{PG}} \newcommand{\Var}{\opstyle{Var}} \newcommand{\tpc}{\;|||\;} \newcommand{\dpc}{\;||\;} \newcommand{\hand}[1]{\;||_{#1}\;} \newcommand{\Val}{\opstyle{Val}} \newcommand{\Chan}{\opstyle{Chan}} \newcommand{\capacity}{\opstyle{cap}} \newcommand{\Comm}{\opstyle{Comm}} \newcommand{\CS}{\opstyle{CS}} \newcommand{\len}{\opstyle{len}} \newcommand{\trace}{\opstyle{trace}} \newcommand{\Traces}{\opstyle{Traces}} \newcommand{\exinf}{\stackrel{\scriptstyle\infty}{\exists}} \newcommand{\Set}{\opstyle{Set}} \newcommand{\Stack}{\opstyle{Stack}} %\newcommand{\bool}{\opstyle{boolean}} \newcommand{\State}{\opstyle{State}} \newcommand{\BadPref}{\opstyle{BadPref}} \newcommand{\MinBadPref}{\opstyle{MinBadPref}} \newenvironment{mybox}[1]{% \begin{footnotesize}% \color{red}% \begin{tabular}{@{}|c|@{}}% \hline\\[-2.5mm]% \begin{minipage}{#1}% \color{black}% }{% \end{minipage}% \\[-2.5mm] \\ \hline% \end{tabular}% \end{footnotesize}% } \newenvironment{mycbox}[1]{% \begin{center}% \begin{mybox}{#1}% }{% \end{mybox}% \end{center}% } % CIVL-C keywords \newcommand{\cckey}{\$} \newcommand{\cc}[1]{\mbox{\textcolor{blue}{\texttt{\cckey{}#1}}}} \newcommand{\cproc}{\cc{proc}} \newcommand{\cself}{\cc{self}} \newcommand{\cinput}{\cc{input}} \newcommand{\coutput}{\cc{output}} \newcommand{\cspawn}{\cc{spawn}} \newcommand{\cwait}{\cc{wait}} \newcommand{\cassert}{\cc{assert}} \newcommand{\ctrue}{\cc{true}} \newcommand{\cfalse}{\cc{false}} \newcommand{\cassume}{\cc{assume}} \newcommand{\cwhen}{\cc{when}} \newcommand{\cchoose}{\cc{choose}} \newcommand{\cchooseint}{\cc{choose{\U}int}} \newcommand{\cinvariant}{\cc{invariant}} \newcommand{\crequires}{\cc{requires}} \newcommand{\censures}{\cc{ensures}} \newcommand{\cresult}{\cc{result}} \newcommand{\cat}{\texttt{@}} \newcommand{\ccollective}{\cc{collective}} \newcommand{\cheap}{\cc{heap}} \newcommand{\cscope}{\cc{scope}} \newcommand{\cregion}{\cc{region}} \newcommand{\cmalloc}{\cc{malloc}}