Note
These notes are based on a summary of the paper I found online!
How can we construct a state graph for use with model checking in cases where systems have infinite state space?
This paper proposes a method based on abstract interpretation. Specifically, this paper was the first to propose the predicate-based representation used later by Lazy abstraction: representing sets of program states in terms of state predicates that are true at that point!
TODO
There’s a lot more here. I’m tired. I haven’t gone through it.