We formalize stuttering equivalence in Isabelle/HOL. Our development relies on the notion of a stuttering sampling function that identifies blocks of identical sequence elements.
@InProceedings{merz:stuttering-equivalence, author = {Stephan Merz}, title = {Stuttering Equivalence}, journal = {Archive of Formal Proofs}, month = may, year = 2012, note = {\url{http://afp.sf.net/entries/Stuttering_Equivalence.shtml}, Formal proof development}, ISSN = {2150-914x}, }