Verifying Temporal Properties of Reactive Systems by Transformation

Geoff Hamilton
(School of Computing, Dublin City University)

We show how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. In particular, we show how the program transformation technique distillation can be used to transform reactive systems specified in a functional language into a simplified form that can subsequently be analysed to verify temporal properties of the systems. Example systems which are intended to model mutual exclusion are analysed using these techniques with respect to both safety (mutual exclusion) and liveness (non-starvation), with the errors they contain being correctly identified.

In Alexei Lisitsa, Andrei P. Nemytykh and Alberto Pettorossi: Proceedings of the Third International Workshop on Verification and Program Transformation (VPT 2015), London, United Kingdom, 11th April 2015, Electronic Proceedings in Theoretical Computer Science 199, pp. 33–49.
This work was supported, in part, by Science Foundation Ireland grant 10/CE/I1855 to Lero - the Irish Software Engineering Research Centre (, and by the School of Computing, Dublin City University.
Published: 7th December 2015.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: