GdT programmation / séminaire IRILL / séminaire APR
Cubicle : a model checker for parameterized array-based transition systems.
Giovedì 9 novembre 2017Sylvain 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.
Maggiori dettagli qui …
Emmanuel.Chailloux (at) nulllip6.fr