Séminaires
Séminaire du 4 Décembre 2009
Lieu
ENS de Cachan, amphithéatre Fonteneau, Bâtiment d'Alembert: comment y aller
Programme
14h00-15h00: Stefan Schwoon LSV, ENS Cachan & INRIA, Verification of Java programs using jMoped
Abstract: Pushdown systems are a convenient model for programs with recursive procedures. The talk will give an introduction into pushdown model checking and present the tool jMoped, which exploits the resulting theory and acts as a frontend for verifying Java programs.
Following this, the talk will present an extension of the underlying theory to multithreaded programs with shared memory. The resulting reachability problem is undecidable in general, and one approximative technique that has been proposed is to use context-bounded reachability instead. However, the computational cost even for this approximation is prohibitive in general. The talk will discuss a symbolic approach to context-bounded reachability, which seeks to alleviate the problem.
15h00-15h30 : A. Hamez (UPMC), 10^2000 états et au-delà
Abstract: L'avènement des BDD il y a plus de 15 ans a été une véritable révolution pour le model checking en permettant le stockages de grands espace d'états. Depuis leur succès s'est affirmé d'année en année. Toutefois, ils montrent vite leurs limites dans le cas de systèmes réparti. De plus, les manières habituelles de manipuler les BDD sont trop "monolithiques", empêchant ainsi d'éventuelles introspections permettant d'optimiser ces manipulations.
Les Data Decision Diagrams (DDD) ont apporté une grande souplesse avec des chemins de taille variable et un mécanisme d' évaluation basé sur des homomorphismes. Les Hierarchical Set Decision Diagrams (SDD) les ont étendus en apportant la hiérarchie. Ciardo et al. ont introduit en 2001 un mécanisme d'évaluation optimisé appelé "saturation". Celui-ci permet des gains d'ordre exponentiel, mais il requiert des connaissances approfondies sur les diagrammes de décision manipulés.
Nous proposons une méthode, appliquée aux SDD, permettant d'automatiser la saturation. Nous nous basons pour cela sur les homomorphismes. Cette méthode permet aux concepteurs de model checkers de n'ecrire que leur "code métier" sans se soucier de l'adapter à la saturation..