Deductive verification of the Sliding Window Protocol. - D. A. Chkliaev; Valery A. Nepomniaschy (Autom. Control. Comput. Sci., 2013)