%! TEX program = xelatex
\documentclass[aspectratio=169]{beamer}
%\usepackage[utf8]{inputenc}
%\usepackage{times}
\usepackage{amsthm}
%\usepackage{amssymb}
%\usepackage{amsmath}
%\usepackage{wasysym}
%\usepackage{tcolorbox}
\usepackage{graphicx}

\usepackage{listings}
\input{../common/fontsetup}
\input{../common/scalalistings}
%\input{../common/boxes}
\input{../common/mathsetup}

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

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

\begin{document}
%\maketitle

\begin{frame}
  \frametitle{Impact of Verification: Software Disasters}
  \begin{itemize}
    \item Ariane 5 rocket maiden flight explosion: \url{http://www.inf.ed.ac.uk/teaching/courses/seoc/2008_2009/resources/ariane5.pdf}
    \item Mars Polar orbiter loss: \url{https://en.wikipedia.org/wiki/Mars_Polar_Lander}
    ''most likely cause of the mishap was a software error that incorrectly identified vibrations''
    \item Accidents in various Boeing models (777, 737 MAX, \ldots)
    \item Northeast blackout of 2003: \url{https://en.wikipedia.org/wiki/Northeast_blackout_of_2003} (race condition)
    \item Radio therapy machine Therac-25: \url{https://en.wikipedia.org/wiki/Therac-25}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Successful Companies and Startups}
  \begin{itemize}
    \item AbsInt products, many originally from academia: \url{https://www.absint.com/products.htm}
    \begin{itemize}
      \item Verified control software of Airbus 340, 380 using ASTR\'EE static analyzer
      \item Formally proven correct C compiler CompCert (originally by Xavier Leroy)
      \item worst-case execution time analysis, \ldots
    \end{itemize}
    \item Formally verified microkernel seL4 and stack built on top by Data61 (formerly Nicta), used Isabelle
    \item Coverity static analysis company prevent acuired for USD 380M by Synopsis
    \item Jasper Design Automation acquired by Cadence
    \item Semmle datalog analysis, acquired by GitHub
    \item Monoidics: acquired by Facebook, running analysis on facebook phone client
    \item Microsoft Static Driver Verifier: shipped in 2000-s as part of driver validation
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Transition System}

  They are similar to finite-state machines

  Define transition system as $(S, I, r, A)$:
  \begin{itemize}
    \item $S$ - the set containing all states of the system.  \\
    If $S$ is finite, we have a \emph{finite-state system}
    \item $I \subseteq S$ is the set of possible initial states of the system
    \item $r \subseteq S \times A \times S$ - transition relation; $(s,a,s') \in r$ means: \\
           with the environment signal $a$, system can move in one step from state $s$ to $s'$ \\
           \begin{itemize}
           \item we mostly assume that $a$ is the input to the system
           \item in the special case that $r : S \times A \to S$, we say the system is \emph{deterministic}
           \end{itemize}
    \item $A$ - set of signals with which the system communicates with the environment
  \end{itemize}
  
  To establish that a system is well behaved we often introduce a set of error states $E \subseteq S$
  that we never want the system to reach, as well as its complement, the set $G \subseteq S$ of good states.
\end{frame}

\newcommand{\st}[1]{\fbox{$s_{#1}$}}
\newcommand{\inp}[1]{\downarrow \mbox{$a_{#1}$}}
\begin{frame}
  \frametitle{A Trace of the System $M = (S, I, r, A)$}

  A finite or infinite sequence $s_0,a_0,s_1,a_1,s_2,\ldots$
  starting from $s_0 \in I$ with steps given by $r$:

  \[\begin{array}{cc}
    \st{0}  & s_0 \in I \\
    \inp{0}  & a_0 \in A \\
    \st{1}  & (s_0,a_0,s_1) \in r \\
    \inp{1}  & a_1 \in A \\
    \st{2}  & (s_1,a_1,s_2) \in r \\
    \ldots
  \end{array}\]
  In general, we require $(s_i,a_i,s_{i+1}) \in r$ for all $i$ in the length of the sequence.

  If the trace is finite, we assume it ends with a state $s_n$ and call $n$ its length.

  $Traces(M)$ is the set of all traces of $M$

  Reachable states $Reach(M)$: states $s_n$ for which there exists
  a trace that ends in $s_n$,

  $Reach(M) = \{ s_n \mid \exists n. \exists (s_0,a_0,s_1,a_1,\ldots,s_n) \in Traces(M) \}$
  
%  We could also add observation function $o : S \to V$ and map all states in trace with it
%  (we may not be able to observe everything about the system).
\end{frame}

\begin{frame}
  \frametitle{Algorithm: Explicit-State Reachability Checking}
  
  \begin{itemize}
  \item Input: $M = (S, I, r, A)$ where $S$ is \textbf{finite}, $E \subseteq S$ (error states)
  \item Output: \begin{tabular}[t]{l}
    either a $(s_0,a_0,s_1,a_1,\ldots,s_n) \in Traces(M)$ where $s_n \in E$, or \\
    the answer ``Safe'' if no such trace exists
  \end{tabular}

  \item Idea: graph reachability from nodes in $I$, following edges in $(s,a,s') \in r$
  as long as we have not seen $s'$ before
  \item To be able to report the trace, build a directed reachability graph of explored edges (never create cycles or duplicate nodes)
  \item If no edge in $r$ leads to a previusly unexplored node, we stop \\
   (this must eventually happen because $S$ is finite)
  \end{itemize}
\end{frame}


\begin{frame}
  \frametitle{Explicit-State Reachability Checking Algorithm: Graph Search}

  Graph reachability using a work list
  \begin{itemize}
    \item Input: $M = (S, I, r, A)$ where $S$ is \textbf{finite}, $E \subseteq S$ (error states)
    \item Output: \begin{tabular}[t]{l}
      either a $(s_0,a_0,s_1,a_1,\ldots,s_n) \in Traces(M)$ where $s_n \in E$, or \\
      ``safe'' if no such trace exists
    \end{tabular}
      
    For efficiency, differentiate three sets of nodes in a graph:
    \begin{itemize}
      \item set of all nodes
      \item exlored nodes: whose all successors we have explored
      \item frontier nodes (worklist): we have explored them but not their successors
    \end{itemize}
    Key operation: take a frontier node $s$, add all of its unexplored non-frontier successors to the frontier, move $s$ to explored.

  \end{itemize}
  
\end{frame}

\begin{frame}
  \frametitle{Exercise 1: Bounded Counter}

  Consider a system with $S = \{0,1, 2, \ldots, 6\}$ that takes signals $A = \{+,-\}$ with initial state $0$ and
  counts up by 2 on $+$ and down by 2 on $-$ but never goes below $0$ or above $6$ (stays in the state if needed). 
  Write down the transition system definition and
  prove that the state $E = \{ 3 \}$ is not reachable using explicit-state reachability algorithm. Draw the reachability graph.

  \vspace*{6cm}
\end{frame}

\setbeamercolor{coloredboxstuff}{fg=black,bg=white!70!green}

\begin{frame}
  \frametitle{Simplified Transition Relation and Reachable States}

  Let  $M = (S, I, r, A)$ be a transition system. 
  
  Define $\bar r = \{ (s,s') \mid \exists a \in A. (s,a,s') \in r \}$ 
  
  Note: even if $r$ is deterministic, $\bar r$ can become non-deterministic
   
  \ \\

  \begin{beamercolorbox}[wd=0.9\textwidth,sep=1em]{coloredboxstuff}

    Composition of relations: $r_1 \circ r_2 = \{ (x,z) \mid \exists y. (x,y) \in r_1 \land (y, z) \in r_2\}$

  Iteration (paths of length $n$): $r_1^0 = \Delta = \{(x,x) \mid x \in S\}$, \ \ $r_1^{n+1} = r_1 \circ r_1^n$

  Transitive closure of $r_1$:
  \[ 
      r_1^* = \bigcup_{n \ge 0} r_1^n        \hspace*{1cm} \mbox{relates endpoints of all finite paths in graph given by $r_1$}
  \]
  Image of a set under relation: $r_1[X] = \{ y \mid \exists x \in X. (x,y) \in r_1 \}$
  \end{beamercolorbox}

  \begin{theorem}
    $Reach(M) = (\bar r)^*[I]$  \ \ (end points of all finite paths starting in $I$)
  \end{theorem}

\end{frame}

\begin{frame}
  \frametitle{Reachable States Using post}

  $M = (S,I,r,A)$

  \ \\

  If $X \subseteq S$, define $post(X) = {\bar r}[X]$

  \ \\

  Define $post^0(X) = X$, $post^{n+1}(X) = post(post^n(X))$

  \ \\

  \begin{theorem} 
    \[
      \bigcup_{n \ge 0} post^n(I) = Reach(M)
    \]
  \end{theorem}
  Proof (by swapping existential quantifiers in definitions of image, composition, and $\bigcup$):
  \[
    \bigcup_{n \ge 0} post^n(I) = \bigcup_{n \ge 0} {\bar r}[\ldots{\bar r}[I]\ldots] = 
    \bigcup_{n \ge 0} {\bar r}^n[I] = \left(\bigcup_{n \ge 0} {\bar r}^n\right)[I] = {\bar r}^*[I]
  \]

\end{frame}

\begin{frame}
  \frametitle{Invariant and Inductive Invariant}

  \textbf{Invariant} $P$ of the system $M$ is any superset of reachable states: $Reach(M) \subseteq P$.
  \begin{itemize}
  \item $P$ is a property satisfied by all reachable states \\
  (though not all states in $P$ need to be reachable).
  \item In every trace, by definition $s_i \in Reach(M) \subseteq P$. So the 
  property $s_i \in P$ remains in-variant (does not change) as the system makes a step from $i$ to $i+1$
  \end{itemize}

  \ \\

  \textbf{Inductive invariant} $Ind$ is a set $Ind \subseteq S$ that satisfies the following:
  \begin{itemize}
    \item $I \subseteq Ind$ (holds initially)
    \item if $s \in Ind$ and $(s,a,s') \in r$, then $s' \in Ind$
  \end{itemize}
  Exercise: prove that every \textbf{inductive invariant} is an \textbf{invariant}.

  \ \\

  For an invariant $P$, $Ind$ is an \textbf{inductive strengthening} of $P$ if $Ind$ is an inductive invariant and $Ind \subseteq P$ 
  ($Ind$ is an inductive hypothesis that proves $Reach(M) \subseteq Ind \subseteq P$)
\end{frame}

\begin{frame}
  \frametitle{Invariants in Bounded Counter}

  Consider again the bounded counter system $M = (S,I,r,A)$ with  $S = \{0,1, 2, \ldots, 6\}$ and $A = \{+,-\}$.

  Let $G_1 = S \setminus \{ 3 \} = \{ 0, 1, 2, 4, 5, 6\}$
  \begin{itemize}
    \item Is $G_1$ an invariant? Prove or disprove.
    \item Is $G_1$ an inductive invariant? Prove or disprove.
  \end{itemize}

  Same question for $G_2 = \{ 4, 5, 6 \}$ 

  Same question for $G_3 = \{ 0, 2, 4, 6 \}$

  \ \\

  \pause
  \ldots
  {\Large
  \begin{tabular}{c|c|c}
    set    & invariant? \hspace*{1cm} & inductive invariant? \\ \hline
    $G_1$  &    yes                   & no \\
    $G_2$  &    no                    & no \\
    $G_3$  &    yes                   & yes \\
  \end{tabular}
  }
\end{frame}

%% \begin{frame}
%%   \frametitle{Checking Inductive Invariants in Stainless}

%%    \lstinputlisting[language=scala]{LoopInv-lst.scala}

%% \end{frame}

\end{document}
