The Scarpaz.
The Scarpaz Site
:: Your unreliable online reference documentation on the Scarpaz. ::
:: Via malfidinda reta dokumento de referenco pri la Skarpac. ::

Navigation: > [Home page] > [Attic] > [trio-pvs] [Alphabetical Index]     [Tree View]

TRIO formal proofs in PVS

Note: what appears here is what I prepared as a project for the "Theoretical Foundations of Computer Science II" a course I attended at Politecnico di Milano, which is associated to the "Formal Methods" course at the University of Illinois (as EECSxxx?).

[Click here to download the paper archive (237k, Postscript format)]

Overview

In this paper I address the problem of trying to formally prove the TRIO theorems within the PVS environment. The paper contains a human-written introduction to the proofs, with some reasoning and the justification for some choices I made, and the the full log of the proofs themselves, which should be used only as a reference to check the consistency and the correctness of the very details of my work.

The theorems I will try to prove are taken from Felder, Mandrioli, Morzenti, "Proving properties of real-time systems through logical specifications and Petri net models". .

MajaMaja is powered by the Tcl Language. [jump to top of page]

The above document was last modified on 2004-04-16 14:47:33; page last updated on 2010-07-02 at 21:22:34.
Document size: 1233 bytes, plus related data up to 238 kbytes.

Contents:

 
trio_pvs.ps File : trio_pvs.ps 236 kbytes 2000-06-18

Navigation: > [Home page] > [Attic] > [trio-pvs] [Alphabetical Index]     [Tree View]

MajaMaja is powered by the Tcl Language. [jump to top of page]
This page was last updated on 2010-07-02 at 21:22:34.
This site was automagically generated by MajaMaja version 0.298, a simple and easy to use web content manager written in Tcl by scarpaz <scarpaz@scarpaz.com>.