Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908783125463040 |
|---|---|
| author | Zhang, Cheng Fu, Qiancheng Ji, Hang Del Valle, Ines Santacruz Silva, Alexandra Gaboardi, Marco |
| author_facet | Zhang, Cheng Fu, Qiancheng Ji, Hang Del Valle, Ines Santacruz Silva, Alexandra Gaboardi, Marco |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_09986 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT Zhang, Cheng Fu, Qiancheng Ji, Hang Del Valle, Ines Santacruz Silva, Alexandra Gaboardi, Marco Programming Languages Logic in Computer Science 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. |
| title | Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2601.09986 |