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.