Initial release corresponding to the Coq formalization and OCaml tool described in the paper Practical Machine-Checked Formalization of Change Impact Analysis, accepted to TACAS 2020. Supports Coq 8.9 and OCaml 4.07.1, and requires Mathematical Components 1.7.0.
Note that names of some Coq definitions and lemmas in the paper have been shortened for space reasons. The key name mappings are as follows:
chk_V'_complete(Section 4.2) is
chk_V'_sound(Section 4.2) is
connect_top_bot(Section 5.2) is
in_p'(Section 5.2) is
impacted_fresh_V'_sub_eq(Section 5.2) is