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

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

09.11.2017
Докладчики : 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.

Более подробно …
Emmanuel.Chailloux (at) nulllip6.fr
Mentions légales
Карта сайта