Failing with Purpose: Dangling Coverage-Guided Negative Test Generation from a Mechanized P4 Type System

This is an artifact for paper "Failing with Purpose: Dangling Coverage-Guided Negative Test Generation from a Mechanized P4 Type System." The artifact includes the mechanized P4 type system, the SpecTec framework for analyzing and executing the mechanized type system, the fuzzer for generating negative P4 type checker tests, scripts for reproducing the evaluation results, and the evaluation data. The following files and directories are included in the artifact: • README: Overall instructions on how to evaluate the artifact. • REQUIREMENTS: Software dependencies for the artifact. • INSTALL: Step-by-step installation instructions, either using Docker or building locally. • LICENSE: Licensing information for the artifact. • data/: Evaluation data for RQ1, 2, and 4. • rq1,2,4,5.sh: Scripts for reproducing the evaluation results for RQ1, 2, 4, and 5. • BUG: List of compiler and soundness bugs found, reported in RQ3. • spec/, spec-mini/: Mechanized P4 type system specifications, including the full and simplified version for the running example. • p4spec/: The SpecTec framework source code. • p4c/: The p4c compiler source code (v1.2.5.6), with modifications for RQ5.