Errata for Chapter 16 "Combining Model Checking and Data-Flow Analysis"
of the Handbook of Model Checking

- page 503, paragraph "Semi-lattices":
    Replace           "subset M ⊆ E"
    by      "non-empty subset M ⊆ E".

- page 505, Alg. 1, between lines 5 and 6:
    Insert  "e := reached(l)".

- page 505, paragraph below Alg. 1:
    Replace "is added    for the program location"
    by      "is assigned to  the program location".

- page 505, paragraph below Alg. 1:
    Replace "we extend e' ⋢  reached(l′) to return false if reached(l')"
    by      "we extend e' ⊑  reached(l′) to return false if reached(l')".