Verification of TCP packet reordering from libflowmanager with minor changes to code for verification purposes (documented in code). Some small dependencies from libtrace are also included and modified similarly.
To verify, install Verifast and run the command
verifast -disable_overflow_check src/tcp_reorder.c
There will be "dead code" warnings; these are expected and documented in the code (which is unmodified as much as possible).
For the sequence number comparison, we used Coq and VST. These files can be verified by installing those tools and using the provided Makefile.