Welcome to the web site for
SVA, part of the site for Bill
Roscoe's book Understanding Concurrent Systems (UCS).
SVA (Shared Variable Analyser) is a front end for FDR that allows it to analyse concurrent programs using the shared variable model.
It is described in Chapters
and 19 of UCS as well as in
documentation on this site. It comes in two parts, a CSPM
written by Bill
Roscoe, and a front end written by David
that plays the roles of GUI, parser and error interpreter.
It has now been updated by
Gibson-Robinson and Bill to make it compatible with FDR3, in a way
that is essentially functionally equivalent from the user perspective, though the internal plumbing is different.
SVA2 (the FDR3 version) is the second general release of SVA. Please let us know of any bugs or problems you may find.
We would be most interested to hear if you either use SVA as part of a course or achieve any interesting results with it.
SVA and its sources may
be downloaded and used freely subject
to the condition that the authors and Oxford University give no
warranty whatsoever about its functionality. Note that in
to use SVA you will require FDR3, which has separate
availability and licence arrangements.