{
  "annotation_id": "a522f2e7-04c9-4e8a-97f6-ac3fbfba8d71",
  "date_created": "2026-02-17T05:53:24.223000Z",
  "date_modified": "2026-02-17T05:53:24.223000Z",
  "file_hash": "cf31422c26bea89689297399776efd742837ddbd0b482a087135bb2d5747fa58",
  "private": false,
  "record": {
    "abstract": "This paper presents several efficient decision procedures for trace equivalence of GKAT automata, which make use of on-the-fly symbolic techniques via SAT solvers. To demonstrate applicability of our algorithms, we designed symbolic derivatives for CF-GKAT, a practical system based on GKAT designed to validate control-flow transformations. We implemented the algorithms in Rust and evaluated them on both randomly generated benchmarks and real-world control-flow transformations. Indeed, we observed order-of-magnitude performance improvements against existing implementations for both KAT and CF-GKAT. Notably, our experiments also revealed a bug in Ghidra, an industry-standard decompiler, highlighting the practical viability of these systems.",
    "arxiv_id": "2601.09986",
    "authors": [
      "Cheng Zhang",
      "Qiancheng Fu",
      "Hang Ji",
      "Ines Santacruz Del Valle",
      "Alexandra Silva",
      "Marco Gaboardi"
    ],
    "categories": [
      "cs.PL",
      "cs.LO"
    ],
    "license": "http://creativecommons.org/licenses/by/4.0/",
    "title": "Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT",
    "url": "https://arxiv.org/abs/2601.09986",
    "version": "v1"
  },
  "schema_id": "dorsal/arxiv",
  "source": {
    "execution_id": "c15eb9c8-1ed3-402d-8cad-0ae5e516c8a3",
    "id": "arXiv Dataset",
    "type": "Model",
    "variant": "snapshot-2026-01-17",
    "version": "0.1.0"
  },
  "user_id": 1000002
}