Systematic design of complete abstractions: from semantics to program analysis via model-checking

By: Roberto Giacobazzi

Roberto Giacobazzi
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
giaco@sci.univr.it

Abstract:

Completeness is a desirable feature of any abstraction, formalizing the intuition that, relatively to the approximated observables, there is no loss of information which is accumulated by approximating computations in the corresponding abstract domain. In this talk we consider the problem of making abstract interpretations complete by minimally refining or simplifying abstract domains. We provide a constructive characterization for the least complete refinement and the greatest complete simplification of abstractions relatively to a forward/backward semantics. We show how this theory can be used to derive both effective algorithms for manipulating and comparing abstract interpretations and to better understand the power and limitations of known abstractions in semantics, program analysis and model-checking. We show that compositional semantics abstracting maximal traces of a transition system can be systematically derived by making the abstraction complete for trace concatenation. Then, starting from Cousot's proof that state-based model-checking is incomplete with respect to the trace-based semantics of an enhanced mu-calculus, we show that there is no way to make it complete unless having traces them self in the model or by considering straightforward abstractions asserting that a trace is a trace. This proves that any state-based model checking is intrinsically incomplete with respect to the trace-based semantics of the mu-calculus. We conclude by giving a constructive characterization of Clarke et al.'s spurious counterexamples in terms of completeness of the underlying abstract interpretation. This result allows us to understand the structure of the counterexamples produced by a model-checker that can be removed by systematically refining abstractions.

The results presented in the talk have been obtained jointly with: Isabella Mastroeni, Elisa Quintarelli, Francesco Ranzato, and Francesca Scozzari.

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)
  • Incompleteness, counterexamples and refinements in abstract model-checking (SAS'01, 356-373)
  • On the completeness of model checking. By F. Ranzato. (ESOP'01, LNCS, 2028:137-154).
  • Compositionality in the puzzle of semantics (ACM PEPM'02, 87-97)

    • giaco@sci.univr.it