\begin{frame}[allowframebreaks]{deferred}

\begin{enumerate}

    \item User interface to specify model constraint on a pathway
    
    \item Formally verify user constructed pathways
	
    \item Symphony: Analyze accuracy of the predicted recovery time and recovery steps to real data

    \item gethomesafe: Formal verification of graph storage \\
        Assuming that a graph dabtabase is not used, use alloy to verify that graph data is correctly stored and retrieved.

\end{enumerate}

\end{frame}
