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 2, bâtiment C

                             Lundi 15 mai, 10h00

                                --------------
                                Ștefan Ciobâcă
                                --------------

                  Universitatea Alexandru Ioan Cuza din Iasi

                  ==========================================
                  The RMT Tool for Rewriting Modulo Theories
                  ==========================================

We introduce RMT, a tool that combines term rewriting with satisfiability
modulo theories. Rewrite rules in RMT are interpreted modulo a builtin model
so that a rule such as:

f(x * 3 + 1) => g(x)

has the expected meaning in the sense that f(10) will rewrite in one step into
f(3), when f is an uninterpreted function symbol and +, * are the usual
functions over the naturals. RMT contains procedures for proving reachability
and equivalence properties. We show how to use RMT to prove partial
correctness and total/partial equivalence of programs, when the language
semantics is given as a set of rewrite rules. This is work in progress,
jointly with Dorel Lucanu.