\begin{frame}{The goal of this research is to create verified autonomous control systems} \textbf{\underline{ If this research is successful, we will be able to do the following: }} \pause \begin{enumerate} \item \alert<2>{Translate written procedures into discrete control logic} \pause \item \alert<3>{Verify continuous control behavior across discrete mode transitions} \pause \item \alert<4>{Demonstrate autonomous reactor startup with verifiable safety guarantees} \end{enumerate} \end{frame} \begin{frame}{First, we will formalize written procedures into logical statements} \end{frame} \begin{frame}{Second, we will use the logical formulae to generate discrete automata} \end{frame} \begin{frame}{Finally, we will build continuous controllers to move between discrete states} \end{frame} \begin{frame}{Verified autonomous controllers can be created by building this chain of proof of correctness} \end{frame}