<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>9141</REFNUM><AUTHORS><AUTHOR>Ripon,S.</AUTHOR><AUTHOR>Miller,A.</AUTHOR></AUTHORS><YEAR>2009</YEAR><TITLE>Semantic Embedding of Promela-lite in PVS</TITLE><PLACE_PUBLISHED>Proceedings of the 16th Workshop on Automated reasoning</PLACE_PUBLISHED><PUBLISHER>N/A</PUBLISHER><LABEL>Ripon:2009:9141</LABEL><KEYWORDS><KEYWORD>Promela-lite</KEYWORD></KEYWORDS<ABSTRACT>Promela-lite is a specification language that captures the essential features of Promela. Unlike Promela, Promela-lite has a fully defined grammar and type system. This has been used to prove the correctness of automatic symmetry detection techniques used in Promela. We outline work in progress to embed Promela-lite syntax and semantics into the general purpose theorem prover PVS and to use these embeddings to interactively prove language consistency and further properties.</ABSTRACT></RECORD></RECORDS></XML>