@conference {HarrisonMCC:13,
	title = {Automated theorem proving for the systematic analysis of interactive systems},
	booktitle = {Proceedings of the 5th International Workshop on Formal Methods for Interactive Systems},
	year = {2013},
	month = {June},
	publisher = {EASST},
	organization = {EASST},
	abstract = {<p>This paper describes the use of an automated theorem prover to analyse properties of interactive behaviour. It offers an alternative to model checking for the analysis of interactive systems. There are situations, for example when demonstrating safety, in which alternative complementary analyses provide assurance to the regulator. The rigour and detail offered by theorem proving makes it possible to explore features of the design of the interactive system, as modelled, beyond those that would be revealed using model checking. Theorem proving can also speed up proof in some circumstances. The paper illustrates how a theory generated as a basis for theorem proving (using PVS) was developed systematically from a MAL model used to model check the same properties. It also shows how the CTL properties used to check the original model can be translated into theorems. </p>
},
	attachments = {https://haslab.uminho.pt/sites/default/files/michaelharrison/files/harrisonmcc.pdf},
	author = {Michael Harrison and Paolo Masci and Jos{\'e} Creissac Campos and Paul Curzon},
	editor = {Judy Bowen and Steve Reeves}
}