Automatic Techniques for Detecting and Exploiting Symmetry in Model Checking

Alastair Donaldson's PhD thesis obtained from the Department of Computing Science, University of Glasgow, under the supervision of Alice Miller

Welcome to the accompanying website for my PhD thesis.

Dissertation

My PhD dissertation in postscript format.

Code examples and software

From these pages you can download source files for the Promela and SMC code examples used for illustration throughout the thesis.

Also available for download are the three software tools, SPIN-to-GRAPE, SymmExtractor and TopSPIN, which are described in the dissertation. For SymmExtractor and TopSPIN, archives of the Promela specifications used for experimental results are also available.