Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 COQ files for FMSE 2007 article
COQ files for FMSE 2007 article
The following files are the Coq development and extracted program for
the results reported in the article Formal Correctness of Conflict
Detection for Firewalls by Venanzio Capretta, Bernard Stepien,
Amy Felty, and Stan Matwin, appearing in FMSE 2007.
IP addresses are needed for firewall correctness. You need first to
compile bytes_masks.v with the command: coqc bytes_masks to be able to run firewall.v.