Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             Lundi 27 mai, 10h30

                               ---------------
                               Benedikt Becker
                               ---------------

                             LRI et Inria Saclay

         ===========================================================
                            Ghost Code in Action:
         Automated Verification of a Symbolic Interpreter using Why3
         ===========================================================

Symbolic execution is a basic concept for the static analysis of programs. It
amounts to representing sets of concrete program states as a logical formula
relating the program variables, and interpreting sets of executions as a
transformation of that formula.

We are interested in formalising the correctness of a symbolic interpreter
engine, expressed by an over-approximation property stating that symbolic
execution covers all concrete executions, and an under-approximation property
stating that no useless symbolic states are generated.

Our formalisation is tailored for automated verification, that is the
automated discharge of verification conditions to SMT solvers. To achieve this
level of automation, we appropriately annotate the code of the symbolic
interpreter with an original use of both ghost data and ghost statements.

This work was done in the context of the CoLiS project, aiming at the
verification of Debian maintainer scripts, and in collaboration with Nicolas
Jeannerod, Ralf Treinen, Mihaela Sighireanu and Yann Regis-Gianas from IRIF
laboratory, Université de Paris.