*Universität Ulm, Fakultät für Informatik, Abt.
KI* - Our Papers on Using PVS

## Modular Verification of SRT Division

**H. Rueß, N. Shankar, M. Srivas **

**Appeared in: Proceedings of the Conference on Computer-Aided
Verification (CAV'96)**

**Abstract**

We describe a formal specification and verification in PVS for the general
theory of SRT division, and for the hardware design of a specific implementation.
The specification demonstrates how attributes of the PVS language (in particular,
predicate subtypes) allow the general theory to be developed in a readable
manner that is similar to textbook presentations, while the PVS *table*
construct allows direct specification of the implementation's quotient
look-up table. Verification of the derivations in the SRT theory and for
the data path and look-up table of the implementation are highly automated
and performed for arbitrary, but finite precision; in addition, the theory
is verified for general radix, while the implementation is specialized
to radix 4. The effectiveness of the automation derives from PVS's tight
integration of rewriting with decision procedures for equality, linear
arithmetic over integers and rationals, and propositional logic. This example
demonstrates that the resources of an expressive specification language
and of a general-purpose theorem prover are not inimical to highly automated
verification in this domain, and can contribute to clarity, generality,
and reuse.

Available as Postscript
(209 KB) or compressed
Postscript (81 KB).

**BibTeX Entry**

@inproceedings{Ruess96:CAV,
TITLE = {Modular {V}erification of {S}{R}{T} Division},
AUTHOR = {H. Rue{\ss} and N. Shankar and M. K. Srivas},
BOOKTITLE = {Computer-Aided Verification, CAV '96},
EDITOR = {Rajeev Alur and Thomas A. Henzinger},
PAGES = {123--134},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 1102,
MONTH = {July/August},
YEAR = 1996,
ADDRESS = {New Brunswick, NJ}
}

Harald Rueß - March 4, 1997 - Mail
to Webmaster