SVA

Welcome to the web site for SVA, part of the site for Bill Roscoe's new 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.   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 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.
  

 
This is the first general release of SVA, timed to coincide with the publication of UCS. At the time of this release (November 2010) it has only been used by a few people and is therefore relatively untested.  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 FDR, which has separate availability and licence arrangements.