GdT programmation / séminaire IRILL / séminaire APR


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

Thursday, November 9, 2017
Speaker(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.

More details here …
Emmanuel.Chailloux (at)