...ORSH95[*]
PVS is freely available, see the web-site of SRI International http://www.csl.sri.com/sri-csl-pvs.html
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
... PVS[*]
For a PVS dump file with all theories and proofs, see http://www.cs.kun.nl/$\sim$hooman/SpliceSem.html
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
... operators[*]
The test-for-absence operator blocks if the specified value is available in the dataspace.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.