%% Abstract
%% Note: \begin{abstract}...\end{abstract} environment must come
%% before \maketitle command
\begin{abstract}
% The development of type systems and static analyses that automatically bound the complexity
% of programs is an active area of research. Yet because there are inevitably programs
% outside the scope of automated techniques, a variety of interactive
% formal methods have been developed for establishing resource bounds.
% A particularly difficult and important case is
% the complexity of randomized programs.  Prior work has mostly focused
% on \emph{expected} run time bounds. But, these programs are
% often known to offer much stronger performance guarantees: not only do
% they run efficiently on average, but the probability that they deviate
% substantially from their average case behavior is very small. These
% \emph{tail bounds} are particularly important when it comes to the
% analysis of parallel algorithms or space usage.  Despite their
% importance, tight tail bounds on performance are usually quite difficult
% to derive.

We mechanize a theorem by Karp, along with several extensions, that
provide an easy to use ``cookbook'' method for verifying tail
bounds of randomized algorithms, much like the traditional ``Master Theorem'' gives bounds for
deterministic algorithms. We apply these results to several examples:
the number of comparisons performed by QuickSort, the span of parallel
QuickSort, the height of randomly generated binary search trees, and
the number of rounds needed for a distributed leader election
protocol. Because the constants involved in our symbolic bounds are concrete,
we are able to use them to derive numerical probability bounds for various input
sizes for these examples.

% Our work complements a growing body of
% semi-automatic and interactive techniques that have been developed for
% cases where automatic analyses of complexity are not yet feasible.

%Text of abstract \ldots.
\end{abstract}