Séminaires
Séminaire du 6 mars 2015
Lieu
LIP6, salle 25-26/101 comment y aller
Programme
14h00-15h00: Didier Buchs, Université de Genève, "Construire un outil de vérification symbolique depuis une description formelle d’un langage:
Diagrammes de décisions et techniques opérationnelles",
et
15h00-15h30 : Edmundo Lopez, Université de Genève, "Construire un outil de vérification symbolique depuis une description formelle d’un langage:
Traduire une description formelle en techniques opérationnelles".
Abstract (les deux exposés): 
The main limit towards practical model-checking is the combinatorial explosion of the number of states. Among numerous solutions proposed to tackle this problem, Decision Diagrams (DDs) have been proved efficient. They are however low-level data structures: translating a high-level model to them can be cumbersome. Indeed, little work towards their better usability has been undertaken.
We propose an abstract mechanism for the manipulation of DDs, where system transitions are described in terms of rewrite rules. We describe how basic rewrite rules can be assembled through strategies, to describe complex transition relations (e.g. involving various levels of synchronization among parallel components). The strategies and rewrite rules offer a higher-level interface, where the nature of underlying DD is hidden, close to high-level languages used to model concurrent systems. We also describe specific strategies that we use to automatically translate high-level modeling languages (namely Petri Nets and imperative languages) to rewrite strategies, ultimately translated in terms of operations on DDs.