text:
\documentclass{beamer}

\usepackage{hyperref}
\usepackage{listings}
\usepackage{color}
\usepackage{mathtools}
\usepackage{cancel}

\usepackage[backend=bibtex]{biblatex}
\addbibresource{citations.bib}

% http://tex.stackexchange.com/questions/68080/beamer-bibliography-icon
\setbeamertemplate{bibliography item}{%
  \ifboolexpr{ test {\ifentrytype{book}} or test {\ifentrytype{mvbook}}
    or test {\ifentrytype{collection}} or test {\ifentrytype{mvcollection}}
    or test {\ifentrytype{reference}} or test {\ifentrytype{mvreference}} }
    {\setbeamertemplate{bibliography item}[book]}
    {\ifentrytype{online}
       {\setbeamertemplate{bibliography item}[online]}
       {\setbeamertemplate{bibliography item}[article]}}%
  \usebeamertemplate{bibliography item}}

\defbibenvironment{bibliography}
  {\list{}
     {\settowidth{\labelwidth}{\usebeamertemplate{bibliography item}}%
      \setlength{\leftmargin}{\labelwidth}%
      \setlength{\labelsep}{\biblabelsep}%
      \addtolength{\leftmargin}{\labelsep}%
      \setlength{\itemsep}{\bibitemsep}%
      \setlength{\parsep}{\bibparsep}}}
  {\endlist}
  {\item}

% Colours for beamer.
\setbeamercolor{frametitle}{fg=orange}
\setbeamertemplate{itemize item}{\color{orange}$\blacksquare$}
\setbeamertemplate{itemize subitem}{\color{orange}$\blacktriangleright$}

% Colours for syntax highlighting
\definecolor{syntax_red}{rgb}{0.7, 0.0, 0.0} % For strings
\definecolor{syntax_green}{rgb}{0.15, 0.5, 0.25} % For comments
\definecolor{syntax_orange}{rgb}{0.7, 0.4, 0.2} % For keywords

% Haskell settings for lstlisting
\lstset{language=Haskell,
basicstyle=\ttfamily\tiny,
keywordstyle=\color{syntax_orange}\bfseries,
stringstyle=\color{syntax_red},
commentstyle=\color{syntax_green},
numbers=none,
numberstyle=\color{black},
stepnumber=1,
frame=single,
breaklines=true,
numbersep=10pt,
tabsize=4,
showspaces=false,
showstringspaces=false}

\author{
  Beck, Calvin \and Huang, Jiani \and Li, Yishuai
}

\begin{document}

\begin{frame}
  \frametitle{FuzzChick}
  \maketitle
\end{frame}

\section{Introduction}

\begin{frame}
  \frametitle{What is this talk about?}

  \pause

  {\huge FuzzChick!}\\~\\

  \pause

  What is FuzzChick...? \cite{fuzzchick} \\~\\

  \pause

  FuzzChick is an experiment to improve QuickChick using ideas from
  fuzzing. This combines QuickChick with AFL \cite{AFL}.\\~\\~\\

  \pause

  {\huge We'll come back to this...}\\

\end{frame}

\begin{frame}
  \frametitle{QuickChick: A Brief Review}

  QuickChick is a properties based testing framework for Coq. \\

  \begin{itemize}
  \item You build (or derive) generators for data types.
  \item Using those generators you can feed data into test cases.
  \item These test cases can be any arbitrary predicate.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{QuickChick: Pros and Cons}

  So what's great about QuickChick?\\

  \begin{itemize}
  \item Relatively easy to build / derive generators.
  \item Can generate lots of tests for specific properties
    automatically.
  \end{itemize}

  \pause

  What's not so great about QuickChick?\\

  \pause

  \begin{itemize}
  \item Getting \emph{good} generators can be hard!
  \end{itemize}
\end{frame}

\section{Good Generators}

\begin{frame}
  \frametitle{What makes a good generator?}

  The basic idea of what makes a generator ``good'' can vary somewhat
  based on the context. \\

  \pause

  In general you want good coverage. How can you achieve that with
  minimal work?
\end{frame}

\section{FuzzChick}

\begin{frame}
  \frametitle{Finally, FuzzChick!}

  FuzzChick uses AFL to make the choices between constructors for
  building data types for tests.\\

  \pause

  Why is this good?

\end{frame}

\begin{frame}
  \frametitle{FuzzChick Intuition}

  AFL uses DSE to attempt to get good coverage while fuzzing...\\

  \pause

  Maybe we can utilize AFL's smarts to achieve better test coverage.
\end{frame}

\section{Evaluating FuzzChick}

\subsection{FuzzChick and Apache}

\subsection{FuzzChick Coverage}

\begin{frame}
  \frametitle{QuickChick: Now With Coverage!}

  We instrumented QuickChick using bisect\_ppx to get coverage
  estimates!\\~\\

  \pause

  This \emph{mostly} went smoothly...\\~\\

  \includegraphics[width=\textwidth]{bisectbug.png} \\

  \pause

  Maintainer fixed this issue promptly, which was \emph{awesome}!

\end{frame}

\begin{frame}
  \frametitle{QuickChick with coverage... Still needs some polish}

  QuickChick with coverage is cool, but it still does need some
  polish.\\

  \begin{itemize}
    \pause
  \item Includes a lot of excessive extracted Coq code.
    \pause
    \begin{itemize}
    \item Like... All of QuickChick :(.
    \item So, the percentages are a little off.
    \end{itemize}
    \pause
  \item QuickChick generates ``random'' files for each test, and the
    names aren't all that useful
    \begin{itemize}
    \item Modified QuickChick to include test case in name, but still
      not ideal.
    \end{itemize}
  \end{itemize}

  \pause

  But...\\~\\

  \pause

  {\huge It works! We can measure stuff!}
\end{frame}

\begin{frame}
  \frametitle{QuickChick Coverage: ifc-basic}

  Coverage with QuickChick in the ifc-basic example: \\~\\

  \includegraphics[width=\textwidth]{ifccoverage.png} \\

\end{frame}

\begin{frame}
  \frametitle{QuickChick vs FuzzChick: ifc-basic}

  QuickChick: \\~\\

  \includegraphics[width=\textwidth]{ifcquickchick.png} \\~\\

  \pause

  FuzzChick: \\~\\

  \includegraphics[width=\textwidth]{ifcfuzzchick.png} \\~\\

  For some reason it seems that FuzzChick actually gets worse coverage
  than QuickChick on this test case... At least in the time I let it run (I'm not
  terribly patient)
\end{frame}

\begin{frame}
  \frametitle{Why Worse Coverage?}

  \begin{itemize}
  \item Just need to let it run longer?
    \begin{itemize}
    \item AFL needs a while to ``warm up''?
    \end{itemize}
    \pause
  \item QuickChick test already managed to get good coverage in this
    instance, so fuzzing doesn't give us much on top of it?
    \begin{itemize}
    \item Hard to tell what ``good coverage'' is due to the extraneous
      code extracted by QuickChick.
    \end{itemize}
    \pause
  \item Something's not instrumented correctly?
    \pause
  \item This test case, for whatever reason, is fuzzer unfriendly?
    \begin{itemize}
    \item Maybe extracted Coq could be fuzzer unfriendly? Lots of
      inefficient data types like like \texttt{nat} (basically a
      linked list whose length represents a number).
    \item Could result in excessively long paths and hard to solve
      predicates for DSE?
    \item Not sure that having pointers everywhere would be AFL's
      strength...
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Some Further Coverage Testing...}

  Test case:

\begin{lstlisting}[language=Haskell]
Extract Constant unlikely_branch =>
" fun i ->
  if (0 < i)
  then if (i mod 100 == 0)
       then if (i mod 1000 == 0)
            then if (i mod 10000 == 0)
                 then if (i mod 100000 == 0)
                      then if (i mod 1000000 == 0)
                           then if (i < 1000001)
                                then 42
                                else 0
                           else 0
                      else 0
                 else 0
            else 0
       else 0
  else 0
".

Definition always_zero := forAll (choose (0%Z, 9999999%Z)) (fun n => unlikely_branch n =? 0).
\end{lstlisting}

  \pause

  {\large Trying to give AFL a good chance to find the failing branch...}

\end{frame}

\begin{frame}
  \frametitle{Results}

  In the equivalent C code AFL does quite well... \\~\\

  \pause

  QuickChick: \\

  \includegraphics[width=\textwidth]{qc_branches.png} \\~\\

  FuzzChick: \\

  \includegraphics[width=\textwidth]{fuzz_branches.png} \\~\\

  \pause

  Here not so much? FuzzChick doesn't make it as far... \\~\\

  \pause

  Well, in fairness, it does eventually, but it takes a good 30
  minutes. QuickChick was much faster. \\~\\

  \pause

  Suggests maybe the extracted OCaml is harder for AFL to analyze? The
  C branches were discovered very quickly by AFL.

\end{frame}

\begin{frame}
  \frametitle{Performance}
  \begin{itemize}
  \item Fuzzing is an order of magnitude slower than random testing.
  \item Performance bottleneck: disk access.
  \item Experiments to see whether the instrumentation overhead is worth it are
    still in preliminary stages.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Fuzzing a Large Project}
  How do QuickChick and FuzzChick perform on a large scale project? \\~\\

  \pause
  And unfortunately they performed not so well...

\end{frame}

\begin{frame}
\frametitle{Fuzzing a Large Project}
Setting up the experiment: \\~\\

Coq $\xrightarrow[]{???}$ C (Apache) \\~\\

\pause{}

Coq $\xrightarrow[]{Extract}$ \cancel{OCaml $\xrightarrow[]{Link}$ C (Apache)} \\~\\

\pause{}
Coq $\xrightarrow[]{Extract}$ OCaml $\xrightarrow[]{Unix call}$ C (Apache)

\end{frame}

\begin{frame}
\frametitle{Fuzzing a Large Project}

\textbf {Target:} \\~\\
I want the fuzzers to help me capture what is a string that will make the patched Apache run successfully (exit with 0).

\end{frame}

\begin{frame}
\frametitle{Fuzzing a Large Project}

\textbf{Quickchick:} \\~\\

\begin{itemize}
    \item \textbf{Pros:} Quickchick runs pretty fast at generating test cases.

    \item \textbf{Cons:} Quickchick fails to capture the successful case I want when we generate 10000 random strings. (That sounds natural I guess).
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Fuzzing a Large Project}
\textbf{FuzzChick:} \\~\\

\begin{itemize}
    \item \textbf{Pros:} FuzzChick runs AFL and AFL does not generate random string, but it can cheat on having some test script that people wrote.

    \item \textbf{Cons:} It runs pretty slowly (~1.2s per test case). Maybe the string it comes up with is meaningful to the server.
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Fuzzing a Large Project}
    What if we specify a richer spec to Coq? \\~\\
    \pause{}
    Instead of getting the label that whether the Apache exit normally or not, we tried to obtain the stdout string from Apache to Coq. \\~\\
    \pause{}
    It's too messy to specify in the OCaml library that the extracted OCaml function is using. We cannot compile the program. :(  \\~\\
    \pause{}
    Aborted.
\end{frame}

\begin{frame}
\frametitle{Fuzzing a Large Project}

\textbf{Takeaway:} \\~\\
It is not yet very practical to fuzz large real world project with Coq and OCaml.

\end{frame}
\section{Honourable Mentions}

\begin{frame}
  \frametitle{Honourable Mentions: Some Other Stuff We Did}

  \begin{itemize}
  \item Honggfuzz!
  \item Plain AFL!
  \end{itemize}
\end{frame}

\section{End}

\begin{frame}
  \frametitle{Future Work for QuickChick}
  \begin{itemize}
  \item Better support for external program

    QuickChick was originally designed to compile OCaml code extracted from
    Coq. It used system calls to run external programs. To have AFL to analyze
    the instance under test (IUT), we need to link the checker and IUT into one
    instrumented executable.

  \item Rich path coverage analysis

    There are branches in generator, IUT, and checker. We are specifically
    interested in the edge coverage of IUT. However, under current framework,
    the IUT is opaque to analysis.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Conclusion! Questions?}

  \huge{Whew! Questions?}
\end{frame}

\begin{frame}
  \frametitle{References}

  \nocite{*}
  \printbibliography

  These are all good resources! You should look at them!
\end{frame}
\end{document}


text:
%!TEX TS-program = xelatex
%!TEX encoding = UTF-8 Unicode

\documentclass[11pt, a4paper]{article}
\usepackage{fontspec}

% DOCUMENT LAYOUT
\usepackage[margin=1.2in]{geometry}
\setlength\parindent{0in}

% fix for pandoc 1.14
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}

% Reduce spacing in itemize, enumerate and titles
\usepackage{multicol}
\usepackage{enumitem}
\setenumerate{nolistsep}
\setitemize{nolistsep}

% FONTS
\usepackage{xunicode}
\usepackage{xltxtra}
\defaultfontfeatures{Mapping=tex-text} % converts LaTeX specials (quotes'' --- dashes etc.) to unicode
% \setromanfont[Ligatures={Common}, Numbers={OldStyle}]{Palatino}
% \setmonofont[Scale=1.0]{Monaco}
% \setsansfont[Scale=1.0]{Optima Regular}

% HEADINGS and TITLES
\usepackage{sectsty}
\usepackage[normalem]{ulem}
\sectionfont{\sffamily\mdseries\large\underline} % Underlines headings
\setcounter{secnumdepth}{-1} % Removes the numbers before sections
\subsectionfont{\rmfamily\mdseries\scshape\normalsize}
\subsubsectionfont{\rmfamily\bfseries\upshape\normalsize}

\usepackage{titling}
\setlength{\droptitle}{-90pt} % The negative number moves the title closer to the top of the page
\title{Kai Xu} % name Kai Xu
\date{} % Leave blank to remove the date
\author{http://xuk.ai/\\\\
Informatics Forum, 10 Crichton Street \textbar{} Edinburgh, EH8 9AB\\ %Put your address here
+44 (0) 770 771 9899 \textbar{} kai.xu@ed.ac.uk } % put your contact information here

% HYPERLINKS
\usepackage[colorlinks]{hyperref}

% PUBLICATIONS
\usepackage{natbib}
\usepackage{bibentry}

% BEGIN DOCUMENT
\begin{document}
% LOAD mypubs.bib
\bibliographystyle{plain}
\nobibliography{mypubs}
\maketitle
\begin{raggedright}
\href{mailto:kai.xu@ed.ac.uk}{Email} \textbar{}
\href{http://github.com/xukai92}{GitHub} \textbar{}
\href{https://scholar.google.ca/citations?user=kf3C60wAAAAJ}{Google
Scholar}

\subsubsection{About Me}

I am a second year Ph.D Student at
\href{http://www.anc.ed.ac.uk/}{Institute for Adaptive and Neural
Computation}, \href{https://www.ed.ac.uk/informatics}{School of
Informatics}, University of Edinburgh, supervised by
\href{http://homepages.inf.ed.ac.uk/csutton/}{Charles Sutton}. Research
topics that I am interested in include approximate inference, generative
models, deep learning and probabilistic programming.

I am one of the core developers of the \emph{Turing} probabilistic
programming language (\href{https://turing.ml/}{website},
\href{https://github.com/TuringLang/Turing.jl}{GitHub}) in
\href{https://julialang.org/}{Julia}.

\subsubsection{Papers}

\begin{itemize}
\tightlist
\item
  \bibentry{hurwitz2019scalable}
  (\href{https://arxiv.org/abs/1905.12375}{arXiv})
\item
  \bibentry{xu2019rave}
  (\href{http://proceedings.mlr.press/v97/xu19e.html}{abs},
  \href{http://proceedings.mlr.press/v97/xu19e/xu19e.pdf}{pdf},
  \href{http://proceedings.mlr.press/v97/xu19e/xu19e-supp.pdf}{suppl},
  \href{https://github.com/xukai92/RAVE.jl}{code})
\item
  \bibentry{xu2018vrr}
  (\href{https://sites.google.com/view/nipsbnp2018/accepted-papers}{workshop},
  \href{https://drive.google.com/file/d/1x-p13HC0SNTWcWcL_AspBS4OUBEGqn-a/view}{pdf})
\item
  \bibentry{srivastava2018ratio}
  (\href{https://arxiv.org/abs/1806.00101}{arXiv},
  \href{https://arxiv.org/pdf/1806.00101.pdf}{pdf})
\item
  \bibentry{xu2018interpreting}
  (\href{https://arxiv.org/abs/1803.04042}{arXiv},
  \href{https://arxiv.org/pdf/1803.04042.pdf}{pdf},
  \href{http://xuk.ai/darksight/demo/mnist.html}{demo},
  \href{https://github.com/xukai92/darksight}{code},
  \href{http://xuk.ai/darksight/}{website})
\item
  \bibentry{ge2018turing}
  (\href{http://proceedings.mlr.press/v84/ge18b.html}{abs},
  \href{http://proceedings.mlr.press/v84/ge18b/ge18b.pdf}{pdf},
  \href{https://github.com/yebai/Turing.jl}{code},
  \href{http://turing.guru/}{website})
\end{itemize}

\subsubsection{Talks}

\begin{itemize}
\tightlist
\item
  Presenter for ``The Turing Language for Probabilistic Programming.''
  at \emph{Julia Lab}, MIT, MA, USA in June 2019
\item
  Presenter for ``Variational Russian Roulette for Deep Bayesian
  Nonparametrics.'' at \emph{MIT-IBM Research}, MIT, CA, USA in June
  2019.
\item
  Presenter for ``Variational Russian Roulette for Deep Bayesian
  Nonparametrics.'' at \emph{International Conference on Machine
  Learning}, Long Beach, CA, USA in June 2019.
\item
  Copresenter for ``The Turing Language for Probabilistic Programming''
  at \emph{The Inaugural International Conference on Probabilistic
  Programming}, MIT, MA, USA in October 2018

  \begin{itemize}
  \tightlist
  \item
    Introduced the Turing probabilistic programming language.
  \end{itemize}
\item
  Presenter for ``Turing: a Fresh Approach to Probabilistic
  Programming.'' at \emph{JuliaCon 2017}, Berkeley, CA, USA in June 2017
  (\href{https://www.youtube.com/watch?v=DJWNQg7uuCg}{video})

  \begin{itemize}
  \tightlist
  \item
    Introduced a new generic probabilistic programming language named
    Turing.jl.
  \end{itemize}
\end{itemize}

\subsubsection{Experience}

\begin{itemize}
\tightlist
\item
  \textbf{University of Edinburgh} / Tutor for Probabilistic Modelling
  and Reasoning \emph{Jan.~2019 - PRESENT, Edinburgh, United Kingdom}
\item
  \textbf{University of Edinburgh} / Teaching Assistant for Machine
  Learning and Pattern Recognition \emph{Sep.~2018 - Dec.~2018,
  Edinburgh, United Kingdom}
\item
  \textbf{Apple} / Machine Learning Intern \emph{May 2018 - Aug.~2018,
  Cambridge, United Kingdom}
\item
  \textbf{University of Edinburgh} / Teaching Assistant for Design
  Informatics \emph{Oct.~2017 - Dec.~2017, Edinburgh, United Kingdom}
\item
  \textbf{University fo Cambridge} / Research Assistant at Machine
  Learning Group \emph{Nov.~2016 - Jul.~2017, Cambridge, United Kingdom}
\end{itemize}

\subsubsection{Education}

\begin{itemize}
\tightlist
\item
  \textbf{University of Edinburgh} / Ph.D in Informatics: Machine
  Learning \emph{Sep.~2017 - PRESENT, Edinburgh, United Kingdom}

  \begin{itemize}
  \tightlist
  \item
    Being supervised by Dr.~Charles Sutton.
  \end{itemize}
\item
  \textbf{University of Cambridge} / M.Phil in Machine Learning, Speech
  \& Language Technology \emph{Oct.~2015 - Sep.~2016, Cambridge, United
  Kingdom}

  \begin{itemize}
  \tightlist
  \item
    M.Phil thesis supervised by Prof.~Zoubin Ghahramani on probabilistic
    programming.
  \end{itemize}
\item
  \textbf{University of Liverpool} / B.Eng in Computer Science and
  Electronic Engineering \emph{Sep.~2013 - Jun.~2015, Liverpool, United
  Kingdom}
\item
  \textbf{Xi'an Jiaotong-Liverpool University} / B.Eng in Computer
  Science \& Technology \emph{Sep.~2011 - Jun.~2013, Suzhou, China}
\end{itemize}

\subsubsection{Honors \& Awards}

\begin{itemize}
\tightlist
\item
  \textbf{Ph.D Studentship} \emph{2017, University of Edinburgh}
\item
  \textbf{International Undergraduate Student Scholarship} \emph{2013,
  University of Liverpool}
\item
  \textbf{Academic Excellence Award} \emph{2012, Xi'an
  Jiaotong-Liverpool University}
\end{itemize}

\subsubsection{Skills}

\begin{itemize}
\tightlist
\item
  \textbf{Programming} Julia, Python, Java, Scala, MATLAB, Clojure,
  C/C++, HTML, CSS, JavaScript
\item
  \textbf{Tooling} Git, Vim, Markdown, LaTeX
\item
  \textbf{Language} Chinese, Wu Chinese, English
\end{itemize}

\subsubsection{Projects (pre-Ph.D/casual)}

\begin{itemize}
\tightlist
\item
  Mobile Robot Control using ROS
  (\href{./assets/images/fyp.png}{poster})
\item
  DBD Plasma Reactor Power Monitoring System
\item
  Wireless Brain-Computer Interface for Game Control
  (\href{https://www.youtube.com/watch?v=ysmLmQ8NfEY}{video})
\item
  FlatShare (\href{https://github.com/xukai92/flatshare}{code})
\item
  Gravity Snake (\href{http://xuk.ai/gravity_snake/}{demo},
  \href{https://github.com/xukai92/gravity_snake}{code})
\end{itemize}

\subsubsection{Reference}

\begin{itemize}
\tightlist
\item
  \textbf{Dr.~Charles Sutton} School of Informatics, University of
  Edinburgh (\href{mailto:csutton@inf.ed.ac.uk}{email})
\item
  \textbf{Prof.~Zoubin Ghahramani} Department of Engineering, University
  of Cambridge (\href{mailto:zoubin@eng.cam.ac.uk}{email})
\end{itemize}
\end{raggedright}

\end{document}

ext: tex