Incompleteness, Counterexamples and Refinements in Abstract Model-Checking

By: R. Giacobazzi and E. Quintarelli

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


In this paper we study the relation between the lack of completeness in abstract interpretation of model-checking and the structure of the counterexamples produced by the model-checker. We consider two dual forms of completeness of an abstract interpretation: Forward and backward completeness. They correspond respectively to the standard gamma/alpha completeness of an abstract interpretation and can be related with each other by adjunction. We give a constructive characterization of Clarke et al.'s spurious counterexamples in terms of both forward and backward completeness of the underlying abstract interpretation. This result allows us to understand the structure of the counterexamples that can be removed by systematically refining abstract domains to achieve completeness with respect to a given operation. We apply our result to improve static program analysis by refining the model-checking of an abstract interpretation.

Available: DVI, PostScript, BibTeX Entry.

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).