Information Technology Reference
In-Depth Information
4. Burch, J., and Dill, D. Automated verification of pipelined microprocesoor con-
trol. In
Computer-Aided Verification (CAV'94)
(June 1994), D. Dill, Ed., vol. 818
of
LNCS
, Springer-Verlag, pp. 68-80.
5. Davis, M., Logemann, G., and Loveland, D. A machine program for theorem
proving.
Communications of the Association for Computing Machinery 7
(July
1962), 394-397.
6. Goel, A., Sajid, K., Zhou, H., Aziz, A., and Singhal, V. BDD based pro-
cedures for a theory of equality with uninterpreted functions. In
Computer-Aided
Verification (CAV'98)
(1998), A. J. Hu and M. Y. Vardi, Eds., vol. 1427 of
LNCS
,
Springer-Verlag, pp. 244-255.
7. Groote, J., and van de Pol, J. Equational binary decision diagrams. In
Logic for Programming and Reasoning (LPAR'2000)
(2000), M. Parigot and
A. Voronkov, Eds., vol. 1955 of
LNAI
, pp. 161-178.
8. Nieuwenhuis, R., and Oliveras, A. Congruence closure with integer offsets.
In
10h Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR)
(2003), M. Vardi and A. Voronkov, Eds., LNAI 2850, pp. 78-90.
9. Pnueli, A., Rodeh, Y., Shtrichman, O., and Siegel, M. Deciding equality for-
mulas by small domains instantiations. In
Computer Aided Verification (CAV'99)
(1999), vol. 1633 of
LNCS
, Springer-Verlag, pp. 455-469.
10. Rodeh, Y., and Shtrichman, O. Finite instantiations in equivalence logic with
uninterpreted functions. In
Computer Aided Verification (CAV'01)
(July 2001),
vol. 2102 of
LNCS
, Springer-Verlag, pp. 144-154.
11. Shostak, R. An algorithm for reasoning about equality.
Communications of the
ACM 21
(1978).
12. Tseitin, G. On the complexity of derivation in propositional calculus. In
Studies
in Constructive Mathematics and Mathematical Logic, Part 2
. Consultant Bureau,
New York-London, 1968, pp. 115-125.
Search WWH ::
Custom Search