Refining and Compressing Abstract Model Checking

By: A. Dovier, R. Giacobazzi, and E. Quintarelli

Roberto Giacobazzi
Dipartimento di Informatica
Univ. di Verona
Strada Le Grazie 15, Ca' Vignal 2, 37134 Verona (Italy)


For verifying systems involving a wide number or even an infinite number of states, standard model checking needs approximating techniques to be tractable. Abstract interpretation offers an appropriate framework to approximate models of reactive systems in order to obtain simpler models, where properties of interest can be effectively checked. In this work we study the impact of domain refinements in abstract interpretation based model checking. We consider the universal fragment of the branching time temporal logic CTL* and we characterize the structure of temporal formulae that are verified in new abstract models obtained by refining an abstract domain by means of reduced product and disjunctive completion, or by simplifying the domain by their inverse operations of complementation and least disjunctive bases.

Available: ENTCS-source

Related papers:
  • A Unifying View on Abstract Domain Design (ACM Comp. Surveys 28(2), 1996)
  • Refining and compressing abstract domains (ICALP'97, LNCS 1256: 771-781, 1997)
  • Completeness in abstract interpretation: A domain perspective (AMAST'97, LNCS 1349: 231-245, 1997)
  • Complete abstract interpretations made constructive (MFCS'98, LNCS 1450:366-377, 1998)
  • Building Complete Abstract Interpretations in a Linear Logic-based Setting (SAS'98, LNCS, 1998)
  • Making abstract interpretations complete (Journal of the ACM. 47(2):361-416 2000).