Project Github Repo The main Netter compiler is available at https://github.com/arthuraa/netter, while this artifact contains example code and models for case studies from the paper. Extract Instruction This artifact is designed to be executed with VMCAI 2021 Virtual Machine (https://doi.org/10.5281/zenodo.4017292). One important assumption is that you extract the ZIP file content under `/home/vmcai2021`, since we have some implicit dependencies for local package locations. See README.md within the ZIP file for more details. Description This artifact contains the Netter compiler and models for all the cases discussed in the paper. - Section 2: Example in the Overview - Section 4.1: Warm up chain topology - Section 4.2: MPLS - Section 4.3: Load balancer - Section 4.4: CoDef link-flooding defense Moreover, it contains the Coq formalization. The Coq development contains two main results in coq/Imp.v: dead_store_elimP, dead_store_elim_optE, inline_run and inline_rew. The first one says that the dead store elimination pass "dead_store_elim" preserves the semantics of programs. The second one says that an optimized version of "dead_store_elim", "dead_store_elim_opt", computes the same result. The last two say that the inlining pass "inline" preserves the semantics of programs and of computed rewards. These passes were translated by hand to the "deadStoreElimOpt" and "inline" functions of src/Netter/Compiler/Optimize.hs. Please refer to the README.md file for additional details. SHA256 checksum 9281e42609349a0da7d9094b0a5326af1a0e3d5d291892b0a5c3250ccf0cc88c submission.zip