Electronic Appendix

A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules, by Michel St-Martin and Amy P. Felty, In Proceedings of the Fifth ACM SIGPLAN Conference on Certified Programs and Proofs (CPP), 2016 (pdf).

The files run in Coq V8.4. They must be compiled in the order they are listed.

Tactics.v
Core.v
Srac.v
Rules.v
RuleSet.v
Example.v

The code is also available as a zip file.