<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>9240</REFNUM><AUTHORS><AUTHOR>Ripon,S.</AUTHOR><AUTHOR>Miller,A.</AUTHOR><AUTHOR>Donaldson,D.</AUTHOR></AUTHORS><YEAR>2009</YEAR><TITLE>A Semantic Embedding of Promela-Lite in PVS</TITLE><PLACE_PUBLISHED>Proceedings of the Ninth International Workshop on Automated Verification of Critical Systems (AVoCS'09)</PLACE_PUBLISHED><PUBLISHER>N/A</PUBLISHER><LABEL>Ripon:2009:9240</LABEL><KEYWORDS><KEYWORD>Promela-Lite</KEYWORD></KEYWORDS<ABSTRACT>We present a case study in applying mechanical verification via theorem proving to Promela-Lite. We show how the syntax and semantics of Promela-Lite can be embedded in the general purpose theorem prover PVS, so that consistency of the syntax and semantics can be interactively proved.</ABSTRACT><NOTES>To appear (September 09)</NOTES></RECORD></RECORDS></XML>