<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>8029</REFNUM><AUTHORS><AUTHOR>Donaldson,A.F.</AUTHOR><AUTHOR>Gay,S.J.</AUTHOR></AUTHORS><YEAR>2005</YEAR><TITLE>Etch: Enhanced Typechecking for Promela</TITLE><PLACE_PUBLISHED>Proceedings of the SPIN Workshop; LNCS 3639 DOI: 10.1007/11537328_21</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>266-271</PAGES><ISBN>0302-9743</ISBN><LABEL>Donaldson:2005:8029</LABEL><KEYWORDS><KEYWORD>Promela</KEYWORD></KEYWORDS<ABSTRACT>Promela, the specification language of the SPIN model-checker, supports declaration of much static type information; however, SPIN does not make full use of this information when typechecking models. We present Etch, an enhanced typechecking tool for use with Promela/SPIN, which makes use of type inference techniques to detect more type errors at model-building time and therefore increase confidence in the accuracy of models.</ABSTRACT></RECORD></RECORDS></XML>