%! TEX program = xelatex
\documentclass[aspectratio=169]{beamer}
\usepackage{amsthm}
\usepackage{graphicx}
\usepackage{fancybox}
\usepackage{listings}
\input{../common/fontsetup}
\input{../common/scalalistings}
\input{../common/mathsetup}

\input{../common/mysymbols}
\input{../common/constructors}
\input{../common/mybeamer}

\usepackage{tikz}
\usetikzlibrary{automata,positioning,arrows,arrows.meta}
\usepackage{bclogo}

\title{Formal Verification (CS-550)}
\author{Viktor Kuncak, EPFL}
\date{\url{https://lara.epfl.ch/w/fv}}

\nobox
\input{bmc}

\end{document}
