%0 Conference Proceedings
%F r01b
%A Rusu, V.
%T Verifying a Sliding-Window Protocol using PVS
%B Formal Description Techniques (FORTE'01)
%P 251-266
%X We present the deductive verification of safety and liveness properties of a sliding-window protocol using the PVS theorem prover. The protocol is modeled in an operational style which is close to an actual program. It has parametric window sizes for both sender and receiver, and unbounded lossy communication channels carrying unbounded data. The proofs are done using invariant strengthening techniques encoded as PVS automated strategies based on heuristics and decision procedures
%U http://www.irisa.fr/vertecs/Publis/Ps/Forte01.ps.gz
%D 2001