Kinetically Constrained Spin Models (KCSM) are interacting particle systems on integer latticeswhich have been introduced by physicists in the 80’s to model the liquid/glass transition and more generally the "glassy behaviour" occurring in a large variety of systems (colloidal suspensions, vibrated granulars, emulsions, foams...). Each lattice site is either empty or occupied by a particle and the evolution is given by a continuous time Markov process with elementary moves corresponding to the creation/destruction of particles. The key feature is that a move can occur only if the configuration verifies a local constraint which specifies the maximal number of particles in a certain neighbourhood. Extensive numerical simulations indicate that, for proper choices of the constraints, KCSM display a remarkable glassy behavior which makes them particularly appealing for physicists striving for the long-lived open problem of the liquid/glass transition. On the other hand, from a mathematical point of view, KCSM pose very challenging and interesting issues. In fact, the hardness of the constraints induces non-attractiveness, the occurrence of several invariant measures, and the failure of many powerful tools (coercive inequalities, coupling, censoring...). Most importantly, the degeneracy of the rates is not a mere technical obstacle which prevents the use of classic tools. Indeed, the behavior of KCSM is qualitatively different from that of other Glauber dynamics. Peculiar features include: anomalously long mixing times, aging, singularities in the dynamical large deviation function, dynamical heterogeneities, and ergodicity breaking transitions leading to a large variety of amorphous structures. The aim of this seminar is to review the existing mathematical results on KCSM. In particular, we will illustrate recent results on the large time behavior of the stationary process, including the full universality picture in two dimensions. On the way, we will explain the connection of KCSM with another a class of models which has been extensively studied by the probability and combinatorics community: bootstrap percolation cellular automata.