A number of enhancements to model-checking technology, as developed within the VIRES project, are presented and demonstrated on a Medium Access Control protocol.