Séminaires
Séminaire du 30 septembre 2016
Lieu
LSV, Salle Renaudeau dans le Bâtiment Laplace (ENS de Cachan): comment y aller
Programme
14h00-15h00: Hubert Garavel (Inria/LIG)
Part 1: Hubert Garavel (Inria/LIG) "Term Rewrite Systems and the Definition of Signed Integers"
Abstract : Term Rewrite Systems specify computations by means of sorts, constructor and non-constructor operations, and algebraic equations that define the meaning of operations. It is well known since Peano that term rewrite systems allow to easily define natural (i.e., unsigned) numbers using the "zero" and "succ" constructors. There is less consensus, however, on how to define integer (i.e., signed) numbers. We review and compare different solutions that can be found in CADP, CASL, Coq, mCRL2, etc.
Part 2: "Benchmarking Implementations of Conditional Term Rewrite Systems", Hubert Garavel joint work with Imad Arrada and Mohammad-Ali Tabikh
Abstract : Conditional Term Rewrite Systems have been adopted in many algebraic and functional languages, such as Haskell, LNT, LOTOS, Maude, mCRL2, OCAML, Opal, Rascal, Scala, SML MLTON, SML New Jersey, etc. We aim at comparing the performance (wrt memory and CPU time) of these implementations. To do so, we took as a basis the benchmarks developed for the three Rewrite Engine Contests (REC 2006, 2008, and 2010), which we significantly revised and extended, leading to a highly automated approach. We present the early results of our assessments.
15h00-16h00 : Fabrice Kordon (LIP6), "les coulisses du Model Checking Contest"
Abstract : 
depuis 2011, le model checking contest permet aux développeurs d'outils de confronter leur travaux autour d'un benchmark commun ayant pour objectif d'évaluer la manière dont ils les traitent. Au fil des années, le benchmark et les épreuves se sont étoffés et de nombreuses informations peuvent être exraites lors de chaque édition.
L'objectif de cette présentation est de faire le point sur les coulisses du Model Checking Contest en présentan la manière dont il se déroule et les questions scientifiques qui se posent pour la définition des épreuves.