SVA, a tool for analysing shared-variable programs
David Hopkins · 2007
In [6], Roscoe described a prototype compiler that allowed straightforward shared variable programs to be analysed using FDR, by writing a compiler in its CSPM language. This allowed, for example, a high degree of control over atomicity but lacked a proper input language and an interpreter for and counter-examples found. In this paper, we first propose a concrete syntax for the input language, and then describe a GUI which takes this as input, drives a modified compiler and FDR, and then provides a clear explanation of counter-examples in suitable format for users of the language.