Efficient Decision Procedures for Variants of GKAT (Artifact)

ESOP 2026 Artifact for #94 Efficient Decision Procedures for Variants of GKAT This repository contains the artifact for the paper: “Efficient Decision Procedures for Variants of GKAT”. Getting Started Included in the Artifact The artifact includes the source code for the following programs: sym-gkat : Our implementation of on-the-fly symbolic GKAT. sym-cf-gkat: Our implementation of on-the-fly symbolic CF-GKAT. cf-gkat : CF-GKAT by Zhang et al.1 (prior work for benchmarking). sym-kat : Sym-KAT by Pous2 (prior work for benchmarking). We include benchmarks extracted from GNU Coreutils (via blinding) as well as synthetic benchmarks created through random generation. These are located in the benchmarks directory. Disclaimer: Very minor modifications are done to cf-gkat and sym-kat to ensure compatibility with our benchmark input format and to report diagnostic information. These modifications do not affect the core algorithms of the original implementations. Docker Image The artifact is packaged as a Docker image for easy reproducibility. The image is built to support both AMD64 and ARM64 architectures. Alternatively, you can build the Docker image from source by following the instructions in the Building from Source section. Loading the Docker Image To load the Docker image, use the following command, replacing with the path to the appropriate tar file for your architecture: docker load -i Verify that the Image Loaded Correctly (Optional) To verify that the Docker image has been loaded correctly, you can run the following simple tests for each program: Verify sym-cf-gkat: docker run --rm --entrypoint ./sym-cf-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/coreutils/inputs/basename-blind@main.c /benchmarks/coreutils/inputs/basename-decompiled@main.c This command uses sym-cf-gkat to check the equivalence of the blinded and decompiled versions of the main function from the basename program of Coreutils. It should print a JSON output indicating the equivalence result. Verify sym-gkat: docker run --rm --entrypoint ./sym-gkat.exe -v ./benchmarks/:/benchmarks/ esop2026-artifact /benchmarks/synthetic/inputs-sexpr/e50b20p50eq/e50b20p50eq_00.txt This command uses sym-gkat to check the equivalence of a pair of equivalent expressions from the synthetic benchmark e50b20p50eq_00.txt. It should print two lines of output indicating the expected equivalence and the decision result. Important: To ensure that the Docker image functions correctly when benchmarking cf-gkat and sym-kat, we recommend allowing Docker to use at least 12 GB of memory and 4 CPUs. Step-by-step Instructions Coreutils The Coreutils benchmarks are applicable to the following programs: - sym-cf-gkat - cf-gkat Coreutil inputs are located in benchmarks/coreutils/inputs. These benchmark inputs are blinded GNU Coreutil programs and their decompiled versions from Ghidra. They follow the naming convention -blind@ .c for blinded programs and -decompiled@ .c for decompiled versions. Node: The scripts contained in benchmarks/coreutils/scripts are included in the Docker image and should be executed using docker run commands. Running Coreutils Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 7s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./coreutils/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 7s to complete. Benchmark cf-gkat (slow): docker run --rm --entrypoint ./coreutils/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 40 minutes to complete. The plotting script in the analysis section below does not require the full set of cf-gkat data points to function correctly. Coreutils Benchmark Results Benchmark results will be saved in the respective output directories: - sym-cf-gkat with BDD: benchmarks/coreutils/outputs-sym-cf-gkat-bdd - sym-cf-gkat with SAT: benchmarks/coreutils/outputs-sym-cf-gkat-sat - cf-gkat: benchmarks/coreutils/outputs-cf-gkat The output format of sym-cf-gkat is JSON, as shown in the example below: { "results": [ { "name": "cat", "location1": "./benchmarks/coreutils/inputs/cat-decompiled@cat.c:7:6:80", "location2": "./benchmarks/coreutils/inputs/cat-blind@cat.c:7:6:80", "num_bvars1": 42, "num_bvars2": 42, "num_actions1": 58, "num_actions2": 58, "is_equiv": true, "duration": 584 } ], "diff": [], "duration": 11815 } results: An array of results for each function checked. name: The name of the function. location1 and location2: The file locations of the two checked CF-GKAT expressions. num_bvars1 and num_bvars2: The number of tests in each expression. num_actions1 and num_actions2: The number of actions in each expression. is_equiv: A boolean indicating whether the two expressions are equivalent. duration: The time taken (in microseconds) to check the equivalence of this function. diff: An array containing differences if the expressions are not equivalent. duration: The total time taken (in microseconds) for the checker. The output format of cf-gkat is also JSON, as shown in the example below: {"results":[{"name":"main","is_equiv":["Done",true],"duration":1820.0874328613281}],"duration":39803.98178100586} results: An array of results for each function checked. name: The name of the function. is_equiv: Completion status of the function check.Status could be due to Done(bool): successfully checked equivalence (true/false), Unsupported: unsupported control-flow constructs, Timeout: timeout after 2 minutes, OutOfMemory: out of memory with 4GB limit, Failed: other internal errors duration: The time taken (in microseconds) to check the equivalence of this function. duration: The total time taken (in microseconds) for the checker. Analysis of Coreutils Benchmark Results To analyze and plot the benchmark results, use the following command: docker run --rm --entrypoint ./coreutils/scripts/plot_logs.py -v ./benchmarks:/benchmarks/ esop2026-artifact The docker container already has all the required dependencies installed to run the script. All of the necessary log files will be read from the output directories mentioned above. This will generate scatter plots for time and memory usage comparisons between the different tools. The plots will be saved in the benchmarks/coreutils/analysis directory. Synthetic Benchmarks The synthetic benchmarks are applicable to the following programs: - sym-gkat - sym-cf-gkat - cf-gkat (limited set due to scalability issues) - sym-kat The synthetic benchmarks are generated randomly with varying parameters such as the number of actions, number of tests, and expression depth. Each benchmark consists of 100 pairs of expressions to be checked for equivalence. For instance, the benchmark e50b20p50eq contains 100 pairs of expressions where each expression has approximately 50 structural connectives (prefix e50), a maximum of 20 unique boolean variables (prefix b20) per test, and a maximum of 50 primitive actions (prefix p50). The suffix eq indicates that the pairs of expressions are equivalent. The synthetic benchmarks come in two different formats: 1. .c files: These files contain C code that can be used as inputs to sym-cf-gkat and cf-gkat. These files are located in benchmarks/synthetic/inputs-cexpr. 2. .txt files: These files contain KAT expressions in S-expression format that can be used as inputs to sym-gkat and sym-kat. These files are located in benchmarks/synthetic/inputs-sexpr. The benchmarks using these two formats are equivalent. Running Synthetic Benchmarks The benchmark scripts assume that the benchmarks directory is mounted to /benchmarks/ in the Docker container. Benchmark sym-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 80s to complete. Benchmark sym-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 30s to complete. Benchmark sym-cf-gkat using BDD backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_bdd.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-cf-gkat using SAT backend: docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_cf_gkat_sat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 140s to complete. Benchmark sym-kat (slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_sym_kat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: This will take approximately 3.5h to complete. The plotting script in the analysis section below does not require the full set of sym-kat data points to function correctly. Benchmark cf-gkat (very slow): docker run --rm --entrypoint ./synthetic/scripts/benchmark_cf_gkat.sh -v ./benchmarks:/benchmarks/ esop2026-artifact Note: Due the scalability limitation of the original cf-gkat algorithm3, we do not expect it to complete the full set of synthetic benchmarks within a reasonable time frame. For this reason, its data points are not required or used by the analysis scripts below. Synthetic Benchmark Results The benchmark results will be saved in respective log files in the benchmarks/synthetic/logs