Performance analysis and functional verification of the stop-and-wait protocol in HOL
scientific article; zbMATH DE number 5638515