diff --git a/slides.tex b/slides.tex
index 535d247..288354c 100644
--- a/slides.tex
+++ b/slides.tex
@@ -80,7 +80,7 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \title[] {Reliable and Fast DWARF-based Stack Unwinding}
-\author[\slidecountline]{\textbf{Théophile Bastian}\\
+\author[\slidecountline]{\alert{\textbf{Théophile Bastian}}\\
     \textbf{Stephen Kell} \\
 \textbf{Francesco Zappa Nardelli}}
 \date{}
@@ -114,7 +114,7 @@
                 \vspace{-1em}
 
                 \smallskip
-                ONR Vertica \\
+                ONR VerticA \\
                 Google Research Fellowship
             \end{tcolorbox}
         \end{column}
@@ -187,7 +187,7 @@ Segmentation fault.
                 >{\columncolor{Thistle}}l
                 l l l l l l
                 >{\columncolor{Apricot}}l}
-~LOC & CFA & rbx & rbp & r12 & r13 & r14 & r15 & ra \\
+~PC & CFA & rbx & rbp & r12 & r13 & r14 & r15 & ra \\
 0084950 & rsp+8 & u & u & u & u & u & u & c-8 \\
 0084952 & rsp+16 & u & u & u & u & u & c-16 & c-8 \\
 0084954 & rsp+24 & u & u & u & u & c-24 & c-16 & c-8 \\
@@ -236,6 +236,8 @@ Segmentation fault.
   [...]
     \end{lstlisting}
 
+    \pause{}
+
     \begin{itemize}
         \item[\textbf{$\longrightarrow$}] \textbf{\alert{constructed} on-demand
             by a \alert{Turing-complete stack machine}!}
@@ -312,7 +314,7 @@ Segmentation fault.
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Unwinding data as an abstract execution of the assembly}
+\section{Correct by construction unwinding tables: synthesis}
 \sectiontitleframe{}
 
 \newcommand{\tblrowval}[4]{#1 & #2 & \only<2->{#3} & \only<2->{#4} \\}
@@ -350,7 +352,7 @@ Segmentation fault.
                 \begin{itemize}
                     \item the assembly is was generated by a compiler
                     \item which also generated unwinding data
-                    \item and I have a reliable DWARF parser
+                    \item and I have a reliable DWARF interpreter
                 \end{itemize}
 			\end{tcolorbox}
 		\end{textblock*}
@@ -382,7 +384,7 @@ Segmentation fault.
                 \alert{ra = *(\reg{rsp} + 16)}}
             \only<8>{The unwinding table captures an \alert{abstract execution}
             of the code\ldots}
-            \only<9>{\ldots and thus can be \alert{synthesized from the binary}.}
+            \only<9>{\ldots and thus is \alert{redundant with the binary}.}
         \end{overlayarea}
     }
     }
@@ -391,36 +393,25 @@ Segmentation fault.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Unwinding data synthesis from binaries}
 
-%\begin{frame}{Why would synthesis be useful?}
-%    \begin{itemize}
-%        \item As said earlier, \alert{DWARF is complex}
-%        \item Some compilers \alert{do not generate it}: hard to \alert{debug}
-%            \& \alert{profile}.
-%        \item Think of \alert{JIT-compiled assembly} (eg. JVM)
-%        \item \ldots{}or even \alert{hand-written inlined assembly}!
-%            \begin{itemize}
-%                \item Painful enough to write for not bothering with DWARF
-%                \item May not even be known by the programmer, breaks gdb
-%                \item May be wrong (remember Linus!)
-%            \end{itemize}
-%    \end{itemize}
-%\end{frame}
-
-\begin{frame}{How do we actually synthesize?}
+\begin{frame}{Synthesis strategy}
     \begin{itemize}
         \item Upon entering a function, we know
             \[ \cfa = \reg{rsp} - 8
             \qquad \ra = \cfa + 8 \]
-        \item The semantics of each instruction specifies \alert{how it changes \cfa}.
+        \item The semantics of each instruction specifies \alert{how it changes
+            the \cfa}.
             \begin{itemize}
                 \item Heuristic to decide whether we index with \reg{rbp} or
                     \reg{rsp}
             \end{itemize}
-        \item By performing a symbolic execution, we can \alert{synthesize the
+        \item By performing symbolic execution, we can \alert{synthesize the
             unwinding table} line by line.
         \item Control flow: forward data-flow analysis
         \item The fixpoints are immediate, cf article
     \end{itemize}
+
+    \todo{Mettre en boîte}
+    Implemented on top of CMU's \prog{BAP}
 \end{frame}
 
 \begin{frame}{}
@@ -457,7 +448,7 @@ Segmentation fault.
                             >{\columncolor{Thistle}}l
                             l l
                         >{\columncolor{Apricot}}l}
-                        LOC & CFA & rbx & rbp & ra \\
+                        ~PC & CFA & rbx & rbp & ra \\
                         0084950 & rsp+8 & u & u & c-8 \\
                         0084952 & rsp+16 & u & u & c-8 \\
                         0084954 & rsp+24 & u & u & c-8 \\
@@ -501,7 +492,7 @@ Segmentation fault.
         \item \texttt{libunwind-eh\_elf}: alternative implementation using
             \ehelfs{}
 
-        \item[$\leadsto$] almost \alert{``relink-and-play''} for existing projects!
+        \item[$\leadsto$] Same API, almost \alert{``relink-and-play''} for existing projects!
     \end{itemize}
 \end{frame}
 
@@ -519,11 +510,6 @@ Segmentation fault.
             \end{itemize}
 
         \item \alert{Space overhead}: x2.6 to x3 vs. DWARF
-
-            \vspace{2em}
-
-        \item[$\leadsto$] Alternative time/space trade-off, favorable eg. for
-            profiling.
     \end{itemize}
 \end{frame}
 
@@ -531,13 +517,22 @@ Segmentation fault.
 \section*{Conclusion}
 \setcounter{section}{0}
 
-\begin{frame}{A lot of things remain to be done!}
+\begin{frame}{}
+    \vfill
+    \centering
+    \begin{beamercolorbox}[sep=8pt,center,shadow=true,rounded=true]{title}
+        \Large
+        What's next?
+    \end{beamercolorbox}
+    \vfill
+\end{frame}
+
+\begin{frame}{}
     \begin{itemize}
         \item{} Synthesis + compare = verification of unwinding data!
-        \item{} Synthesis could be integrated in compilers: support for inline
-            assembly, fallback, \ldots
-        \item{} Speedup could be implemented in profilers, debuggers,
-            \ldots{}
+        \item{} Integrate synthesis into compilers \& debuggers\\
+            $\rightarrow$ support for inline assembly, fallback method, \ldots
+        \item{} Integrate into \prog{perf} for a faster analysis
         \item{} Probably many more cool things to do!
     \end{itemize}