diff --git a/slides.tex b/slides.tex
index 5eeed96..aa14531 100644
--- a/slides.tex
+++ b/slides.tex
@@ -176,7 +176,7 @@ Segmentation fault.
             \end{lstlisting}
             \pause{}
             \begin{center}
-                \textbf{\Large How does it work?!}
+                \textbf{\Large How does it work?}
             \end{center}
         \end{column}
         \begin{column}{0.35\textwidth}
@@ -194,7 +194,8 @@ Segmentation fault.
         \begin{column}{0.65\textwidth}
             \begin{center}
                 \large\bf
-                How do we get the RA\@?
+                How do we get\\
+                the return address?
 
                 \vspace{2em}
 
@@ -393,7 +394,7 @@ Segmentation fault.
 \end{frame}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Correct by construction unwinding tables: synthesis}
+\section{Correctness by construction:\\*\textbf{synthesis of unwinding tables}}
 \sectiontitleframe{}
 
 \newcommand{\tblrowval}[4]{#1 & #2 & \only<2->{#3} & \only<2->{#4} \\}
@@ -424,15 +425,16 @@ Segmentation fault.
 
 
     {\only<3>{
-		\begin{textblock*}{0.90\textwidth}[0.5,0.5](0.5\paperwidth,0.5\paperheight)%
+		\begin{textblock*}{\textwidth}[0.5,0.5](0.5\paperwidth,0.5\paperheight)%
 			\begin{tcolorbox}[halign=center, colframe=red, colback=Lavender]
 				\large
-				\alert{\bf Assumptions:}
+				\alert{\bf Assumptions}
+                \vspace{0.6em}
                 \begin{itemize}
-                    \item the assembly is was generated by a compiler
-                    \item which also generated unwinding data
-                    \item and I have a reliable DWARF interpreter
+                    \item the compiler generated the unwinding data
+                    \item we have a reliable DWARF interpreter
                 \end{itemize}
+
 			\end{tcolorbox}
 		\end{textblock*}
 	}}
@@ -482,7 +484,8 @@ Segmentation fault.
                 \item Heuristic to decide whether we index with \reg{rbp} or
                     \reg{rsp}
             \end{itemize}
-        \item By performing symbolic execution, we can \alert{synthesize the
+        \item By performing \alert{symbolic execution} with an abstract
+            semantics, we can \alert{synthesize the
             unwinding table} line by line.
         \item Control flow: forward data-flow analysis
         \item The fixpoints are immediate, cf article
@@ -579,12 +582,12 @@ Segmentation fault.
 
 \begin{frame}
     \begin{itemize}
-        \item \alert{libunwind}: \textit{de facto} standard library for
+        \item \alert{libunwind}: most common library for
             unwinding
 
             \bigskip{}
 
-        \item \texttt{libunwind-eh\_elf}: alternative implementation using
+        \item \alert{\texttt{libunwind-eh\_elf}}: modified version to support
             \ehelfs{}
 
         \item[$\leadsto$] Same API, almost \alert{``relink-and-play''} for existing projects!
@@ -597,7 +600,7 @@ Segmentation fault.
 
 \begin{frame}{Performances}
     \begin{center}
-        \Large\bf Speedup vs. libunwind:
+        \Large\bf Unwinding speedup vs.\ libunwind:
         \begin{columns}
             \begin{column}{0.5\textwidth}
                 \alert{x15} on gzip
@@ -635,8 +638,8 @@ Segmentation fault.
         \item{} Synthesis + compare = verification of unwinding data!
         \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!
+        \item{} Integrate into \prog{perf} for online unwinding
+        \item{} Probably many more cool projects!
     \end{itemize}
 
     \vspace{1em}
@@ -715,15 +718,15 @@ Segmentation fault.
 
                 \vspace{1em}
 
-                We cannot hope for an invariant\dots\\
+                We cannot hope for a simple invariant\dots\\
                 but the compiler cannot
                 either.
 
                 \vspace{1em}
 
                 {
-                    \large\alert{$\implies$} the compiler will \alert{fallback to
-                    \reg{rbp}}\\
+                    \large\alert{$\implies$} the compiler will\\
+                        \alert{fallback to \reg{rbp}}\\
                 }
                 even with \lstbash{--fomit-frame-pointer}
             \end{center}