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.