%! 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}}

\begin{document}
\maketitle

\begin{frame}
  \frametitle{Formal Verification}

  Goal: rigorously prove that computer systems ``do what they should do''

  \ \\

  ``do what they should do'' = satisfy a specification

  \ \\

  How?
  
  1. Define a mathematically rigorous notion of a system satisfying a specification

  \ \\

  2. Use combination of automated tools and human effort to construct the proof

  \ \\

  We will learn: how to \textbf{use} and \textbf{build} tools for computer-aided formal verification
\end{frame}

\begin{frame}
  \frametitle{Comparison to Testing}

  We test computer systems and we should.
  But in formal verification, we go beyond: make mathematical models and prove
  that the systems work. \pause This is hard work. 

  \pause

  Why bother? Maybe we can use a \textbf{really fast} fuzz tester?

  Suppose we want to \textbf{test} that addition of two \textbf{Long} integer values is commutative by trying all possible values.

  \lstinputlisting{plus.scala}

  (The values x and y are arbitrary, they may come, e.g., from input.)
  
  Suppose we 
  can run 10 tests every \textbf{nanosecond}. How long to test \textbf{all} cases?

  \pause

  \begin{tabular}{r@{:\ \ \ }l} 
  Number of tests      & $2^{64} \cdot 2^{64} = 2^{128} > 10^{38}$ \\ 
  Seconds              & $10^{28}$ \\
  Days                 & $1.15 \cdot 10^{23}$ \\
  Years                & $3.15 \cdot 10^{20}$ \\
  \end{tabular}

  \pause

  Ten billion times since ``big bang''. \pause Don't even ask about $x+(y+z)==(x+y)+z$
\end{frame}

\begin{frame}
  \frametitle{Feasible Alternative: Automated Theorem Proving}
  
  A modern software verifier has \textbf{built-in} knowledge of commutativity.
  \begin{itemize}
  \item it's a mathematical \textbf{theorem} about integers modulo $2^{64}$
  \item we can also prove theorems about unbounded integers (need infinitely many tests)
  \end{itemize}

  A verifier also uses \textbf{logical rules}, studied in \textbf{formal (mathematical) logic}, to take existing
  theorems, like $x + y = y + x$, and derive new ones, like $x + (a+1) = (a+1) + x$.

  \pause
  Verifiers also use \textbf{automated theorem proving procedures}, which can discover 
  an infinite number of facts using known theorems and rules.
  
  \pause  
  Different kinds of proving procedures, depending on success guarantees:
  \begin{itemize}
  \item decision procedures (linear arithmetic, SAT, bitvectors), proof checkers: algorithms with upper bounds on time
    by which they terminate with yes/no answer
  \item\pause semi-decision procedures (first-order logic provers): no upper bound, but for every theorem
    there exists a time by which they discover that it holds (complete)
  \item\pause heuristics (simplifiers, induction heuristics, type inference): even if formula is valid, they may run forever,
    or say ``do not know''
  \end{itemize}  
\end{frame}

\begin{frame}
  \frametitle{Compiling to Formulas}
  How do we go from program correctness statements to theorems?

  \
  
  \pause  
  Compile programs and properties to formulas! 
  
  We call these formulas \textbf{verification conditions}.

  \

  If verification condition is valid formula, then program satisfies specification.

  \
  
  Analogy:

  \
  
  \begin{tabular}{c|c}
    programming language compiler & verification-condition generator \\ \hline
    program $\to$ machine code    & (program + specification) $\to$ formula \\
  \end{tabular}

  \

  \ \pause
  
  \fbox{program verifier} = \fbox{verification condition generator} $\bigoplus$ \fbox{theorem prover}


\end{frame}

\end{document}
