Verification, Model Checking, and Abstract Interpretation (Springer Berlin Heidelberg, 2020)