Verification of Infinite Systems
This is the home page for the `Verification of Infinite Systems'
project at Edinburgh, which is devoted to the theory and practice of
verifying the correctness of systems with infinite, or potentially
infinite, state spaces.
`Verification of Infinite Systems--theory, methods and applications'
was an EPSRC funded research grant which ran from 1992 to 1995. The
final report on the grant is available
here. Many of the publications referred to are available from the
personal pages of Colin Stirling and Julian Bradfield.
The software resulting from the grant is available for experimental
and research use by academics. It is a proof assistant for doing small
(at present) verifications on Petri nets using the infinite state
tableau method developed in Bradfield's thesis. An
overview of the theory behind the tool and its use may be found
here, and
more detailed references are also available from that page.
Those wishing to use the tool should send email to
viss@dcs.ed.ac.uk to obtain a licence form, and to
obtain access to the source and installation procedures. (The tool is
still dependent upon certain proprietary software; we hope to remove
this restriction, and when we have, the source will be on this page.)
A tutorial introduction to the use of the tool (assuming knowledge of
the theory) is available here. It's
currently missing the figures, but these will soon be linked in, and
also available on this page, in a Web-browsable version.