Osamu Takaki, Makoto Takeyama, Hiroshi Watanabe,

Verification of Transition System Reduction via PVS

We established a pvs-file "tsr.pvs" and its prf-file "tsr.prf" in which we verified the correctness of TSR (Transition System Reduction).
• pvs-file "tsr.pvs"
• prf-file "tsr.pvs" (with a strategy-file "pvs-strategies")
  We also have another pvs-file "abstract_tsr.pvs", which is a more abstract version of the verification of TSR in "tsr.pvs".

• pvs-file "abstract_tsr.pvs"
• prf-file "abstract_tsr.prf"