TITLE: Limiting State Explosion with Filter-based Refinement

AUTHOR: Matthew B. Dwyer and David A. Schmidt 

AFFILIATION: Department of Computing and Info. Sciences 
             Kansas State University

KEYWORDS:
  software verification and validation, abstract interpretation, 
  flow analysis, model checking

ABSTRACT:
  We introduce "filters", an abstract-interpretation variant,
  to incrementally refine a naively generated state space and
  help validate path properties of the space, for example
  via model checking.  Filters can
  be represented equivalently as
    (i)   state-transition-based abstract interpretations,
    (ii)  ``property automata,'' or
    (iii) path formulas in a CTL*-variant.
  We give examples of filters and show their application in the
  FLAVERS static analysis system.