GdT programmation / séminaire IRILL / séminaire APRRSS

Cubicle : a model checker for parameterized array-based transition systems.


09/11/2017
Intervenant(s) : Sylvain CONCHON (LRI - univ Paris-Saclay)
In this talk, I will present Cubicle, a model checker for verifying safety properties of array-based systems, a syntactically restricted class of para­metrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems. After a short presentation of the semantics of its input language, I will present some details about its implementation, mainly its symbolic backward reachability analysis which makes use of Satisfiabilty Modulo Theories. I will conclude with a presentation of current and future works.
Plus d'informations ici
Emmanuel.Chailloux (at) nulllip6.fr
 Mentions légales
Carte du site |