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

• Download SVA.
  
• Download a directory consisting of files to experiment with that implement all the significant shared variable programs discussed in Chapters 18 and 19 and some  related examples.    Most of these are in the SVL language understood by the front end, but a few are in the form used directly by the back end of SVA, namely the file svacomp.csp. Note that to run SVA you must have FDR installed on your computer, as well as a sufficiently recent JAVA implementation for the front end.
  
• View and download documentation.
  
• Download all of the above.
  
• Read a discussion document about SVA and its history.
  

 
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.