Model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modelled by means of ( nite) Kripke structures, as usual. However, while temporal logics which are interpreted \point-wise" describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted \interval-wise" express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). The most well-known interval temporal logic is Halpern and Shoham's modal logic of time intervals HS, which features one modality for each possible ordering relation between a pair of intervals, apart from equality. In the seminar, we provide an overview of the main results on model checking with HS and its fragments under the homogeneity assumption. In particular, we show that the problem turns out to be non-elementarily decidable and EXPSPACE-hard for full HS, but it is often computationally much better for its fragments. We conclude by brie y comparing the expressiveness of HS in model checking with that of LTL, CTL, CTL* and by outlining a generalization of the proposed model checking framework that allows one to use regular expressions to de ne the behavior of proposition letters over intervals in terms of the component states.