Static analysis, abstract interpretation and verification in (constraint logic) programming

We survey some general principles and methodologies for program analysis and verification. In particular, we focus on abstract interpretation and model checking techniques, and on their applications to constraint logic programs