Book cover   SVA

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 18 and 19 of UCS as well as in documentation  on this site. It comes in two parts, a CSPM back end  written by Bill Roscoe, and a front end written by David Hopkins that plays the roles of GUI, parser and error interpreter. 

It has now been updated by Tom 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.

You may

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 order to use SVA you will require FDR3, which has separate availability and licence arrangements.