# CAV 2005 Invited Talk

##
Randomized Algorithms for Program Analysis and Verification

U. of California, Berkeley

### Abstract

Program analysis and verification are provably hard, and we have all
learned not to expect perfect results. We are accustomed to pay this cost
in terms of completeness and algorithm complexity. Recently we have
started to investigate what benefits we could expect if we are willing to
trade off minuscule amounts of soundness. This talk will describe a
number of randomized analysis algorithms which are much simpler, and in
many cases have lower computational complexity, than the
corresponding deterministic algorithms. The price paid is that such
algorithms may, in rare occasions, infer properties that are not true. We
will describe both the intuitions and the technical arguments that allow
us to evaluate and control the probability that an erroneous result is
returned, in terms of various parameters of the algorithm. These
arguments will also shed light on the limitations of such randomized
algorithms.

These randomized algorithms were developed initially for program
analysis, but have applications in automated deduction as well. We will
describe a satisfiability procedure for uninterpreted functions and
linear arithmetic, and compare it experimentally with deterministic
algorithms. We will also show that it is possible to integrate symbolic
and randomized techniques to leverage the benefits of both worlds. In
this class, we will show extensions of randomized algorithms to
inter-procedural analyses, and an integration of boolean decision
diagrams with linear arithmetic and uninterpreted functions.

* George Necula * is Associate Professor of Computer Science at U.C. Berkeley.