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. Code updated to work with Coq 8.4 (January 2015). 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.