*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 15h00--16h00                     *
*                           Salle S16, etage -1                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

***  Vendredi 8 Février 2008, 15h00-16h00 *************************

From Tests to Proofs

Andrey Rybalchenko, Max Planck Institute for Software Systems

Re'sume'/ Abstract:

We describe the design and implementation of a scalable and
automatic invariant generator for imperative programs.  While automatic
invariant generation has been extensively studied from a theoretical
viewpoint as a classical means to program verification, in practice,
existing tools do not scale even to moderately sized programs, as the
constraint space from even small programs is often already too large for
the underlying (non-linear) constraint solving engines.  Our implementation
combines static constraint generation with constraint strengthening and
simplification using information obtained from dynamic and directed
execution of the program.  While the combination of dynamic analysis for
invariant guessing and static analysis has been tried before, most notably
in the Eraser tool, unlike previous work, our algorithm is sound, and for
the class of arithmetic programs and convex invariants over a fixed
template language, relatively complete.  The proposed technique is
applicable for a large variety of program analysis operations, including
computation of merge operators and under-approximation.
Using our implementation, we provide automatic invariants for a set of
arithmetic benchmark programs considered challenging for software model
checking.  In contrast to the un-optimized implementation of the invariant
generation algorithm, our combined static-dynamic implementation is an
order of magnitude faster, and can produce invariants for some examples for
which the un-optimized version fails to terminate.


***  Vendredi  22 Février 2008, 15h00-16h00 *************************

Quantum entanglement analysis based on abstract interpretation

Simon Perdrix, Oxford University Computing Laboratory

Re'sume'/ Abstract:

Entanglement is a non local property of quantum states which has
no classical counterpart and plays a decisive role in quantum information
theory.  Several protocols, like the teleportation, are based on quantum
entangled states.  Moreover, any quantum algorithm which does not create
entanglement can be efficiently simulated on a classical computer.  The
exact role of the entanglement is nevertheless not well understood.  Since
an exact analysis of entanglement evolution induces an exponential
slowdown, we consider approximative analysis based on the framework of
abstract interpretation.  In this paper, a concrete quantum semantics based
on superoperators is associated with a simple quantum programming language.
The representation of entanglement, i.e. the design of the abstract domain
is a key issue.  A representation of entanglement as a partition of the
memory is chosen.  An abstract semantics is introduced, and the soundness
of the approximation is proven.



*********************************************************************
Pour recevoir l'annonce par courrier electronique:
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************