\documentclass[runningheads]{llncs}
\usepackage{isabelle}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{mathpartir}
\usepackage{tikz}
\usepackage{pgf}
\usepackage{pdfsetup}
\usepackage{ot1patch}
\usepackage{times}
\usepackage{stmaryrd}
\usepackage{url}
\usepackage{color}

\titlerunning{BLA BLA}

\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
\renewcommand{\isastyle}{\normalsize\it}%


\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
\renewcommand{\isasymequiv}{$\dn$}
\renewcommand{\isasymemptyset}{$\varnothing$}
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

\definecolor{mygrey}{rgb}{.80,.80,.80}
\def\Brz{Brzozowski}


\begin{document}

\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}
\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}}
\institute{King's College London, United Kingdom \and 
           St Andrews}
\maketitle

\begin{abstract}
\Brz{} introduced the notion of derivatives of regular expressions
that can be used for very simple regular expression matching algorithms.

BLA BLA  Sulzmann and Lu \cite{Sulzmann2014}

{\bf Keywords:} 
\end{abstract}

\input{session}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: