To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Cristal - 03/06/05 - Paris - FR
Vous pouvez vous abonner à nos annonces de séminaires
http://pauillac.inria.fr/seminaires/subscribe.html
S E M I N A I R E
___ .
/ ___ __ /_ _ / /| /| _ __ __ _ _
/ / / /_ / __| / ----- / |/ | / \ /_ / / \ | / __|
|___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/
I N R I A - Rocquencourt
Amphi Turing du bâtiment 1
Vendredi 3 juin, 10h30
-------------
George Necula
-------------
Berkeley University
===========================================================
Randomized Algorithms for Program Analysis and Verification
===========================================================
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.