Lecturecise 17: Predicate Abstraction
Abstract interpretation view: annotated slides
Explanation of reachability trees: reachability tree
Further reading
Slides on Predicate Abstraction
Abstract Interpretation with Conjunctions of Predicates
Powerdomains for Finite Domains
Powerset of Conjunctions of Predicates