Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic

Randal E. Bryant, Steven M. German, Miroslav N. Velev. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log., 2(1):93-134, 2001. [doi]

@article{BryantGV01,
  title = {Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic},
  author = {Randal E. Bryant and Steven M. German and Miroslav N. Velev},
  year = {2001},
  doi = {10.1145/371282.371364},
  url = {http://doi.acm.org/10.1145/371282.371364},
  tags = {e-science, logic},
  researchr = {https://researchr.org/publication/BryantGV01},
  cites = {0},
  citedby = {0},
  journal = {ACM Trans. Comput. Log.},
  volume = {2},
  number = {1},
  pages = {93-134},
}