A complete abstract interpretation framework for coverability properties of WSTS. (English) Zbl 1176.68119

Ganty, Pierre; Raskin, Jean-François; Van Begin, Laurent

Emerson, E. Allen (ed.) et al., Verification, model checking, and abstract interpretation. 7th international conference, VMCAI 2006, Charleston, SC, USA, January 8–10, 2006. Proceedings. Berlin: Springer (ISBN 3-540-31139-4/pbk). Lecture Notes in Computer Science 3855, 49-64 (2006).

Summary: We present an abstract interpretation based approach to solve the coverability problem of well-structured transition systems. Our approach distinguishes from other attempts in that (1) we solve this problem for the whole class of well-structured transition systems using a forward algorithm. So, our algorithm has to deal with possibly infinite downward closed sets. (2) Whereas other approaches have a non generic representation for downward closed sets of states, which turns out to be hard to devise in practice, we introduce a generic representation requiring no additional effort of implementation.
For the entire collection see [Zbl 1097.68002].

MSC:

68Q60

Specification and verification (program logics, model checking, etc.)