Reference:

Tom Melham and Robert B. Jones. Abstraction by symbolic indexing transformations. In Mark D. Aagaard and John W. O'Leary, editors, Formal Methods in Computer-Aided Design (FMCAD), volume 2517 of Lecture Notes in Computer Science, pages 1-18. Springer-Verlag, November 2002.

Abstract:

Symbolic indexing is a data abstraction technique that exploits the partially-ordered state space of symbolic trajectory evaluation (STE). Use of this technique has been somewhat limited in practice because of its complexity. We present logical machinery and efficient algorithms that provide a much simpler interface to symbolic indexing for the STE user. Our logical machinery also allows correctness assertions proved by symbolic indexing to be composed into larger properties, something previously not possible.

Download (please read copyright notice):

PostScript (gzipped)
PDF (auto-translated from PS, may have problems)

BibTeX entry:

@InProceedings{MelhamJones02FMCAD,
  author    = {Tom Melham and Robert B. Jones},
  title     = {Abstraction by Symbolic Indexing Transformations},
  booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
  pages     = {1--18},
  editor    = {Mark D. Aagaard and John W. O'Leary},
  volume    = 2517,
  series    = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  month     = {November},
  year      = 2002,
}