Verification, Model Checking, and Abstract Interpretation - Barbara Jobstmann, K. Rustan M. Leino; Leino, K. Rustan M. (Springer Berlin Heidelberg, 2016)