In this tutorial we show how constraint logic programs (CLP) provide a exible framework for analysis and veri cation of other languages. Here the focus is on analysing imperative programming languages. It is rst necessary to translate a given imperative program into CLP clauses. Di erent approaches to automatic translation based on small-step or bigstep semantics will be shown, along with their advantages and disadvantages. The role of query-answer transforms in the translation process is also presented. The problem of analysing or verifying properties of an imperative program is thus translated into a CLP analysis or veri cation problem. The main CLP analysis technique covered in this tutorial is the computation of approximate models of CLP clauses using abstract interpretation over numeric or symbolic abstract domains. The tutorial contains a survey of analysis and veri cation problems for imperative programs that have been successfully tackled in this way, including veri cation of safety properties in sequential and concurrent programs, termination, resource analysis and shape analysis.