PVS Example: FORTE'97 Tutorial (Osaka, Japan, November 1997) Proof Checking, and Model Checking for Protocols and Distributed Systems with PVS Web page: http://www.csl.sri.com/forte97.html Documents: forte97.dvi.Z and forte97.ps.gz Dump file: cache.dmp Use PVS command M-x undump-file cache.dmp Provides the following theories and associated proof files cache_array: the full protocol specification NOTE: the proof of "invariant" fails (due to the "postpone" command) because the p_safe property is not inductive. It needs to be strengthened (which is what strong_invariant does) cache2: the protocol specificaiton downscaled to just two processors for model checking abs_cache: a finite-state abstraction of the full protocol, also suitable for model checking refinement: establishes that abs_cache is a true abstraction of cache_array