...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.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.