State Transition Assertions

State Transition Assertions (STAs) was developed as part of the SAFEMOS project; a SERC and DTI funded collaboration between INMOS, SRI International, the Oxford University Programming Research Group and the University of Cambridge Computer Laboratory. Below are the two papers on STAs that were published, both in 1994.

A Mechanized Hoare Logic of State Transitions by Mike Gordon. Published in A Classical Mind: Essays in Honour of CAR Hoare, edited by A. W. Roscoe, Prentice Hall International (UK) Ltd. Hertfordshire, UK, 1994.
[http://dl.acm.org/citation.cfm?id=197611]
State transition assertions: a case study by Mike Gordon. Published in Towards Verified Systems, edited by Jonathan Bowen, Elsevier, Real-Time Safety Critical Systems series, Volume 2, October 1994.
[http://lsbu.academia.edu/JonathanBowen/Books/983621/Towards_Verified_Systems]