| Title |
A symmetry-theoretic framework for AI-guided symbolic execution in embedded systems |
| Authors |
Iavich, Maksim ; Kuchukhidze, Tamari ; Lopata, Audrius |
| DOI |
10.3390/sym18071226 |
| Full Text |
|
| Is Part of |
Symmetry.. Basel : MDPI. 2026, vol. 18, iss. 7, art. no. 1226, p. 1-29.. ISSN 2073-8994 |
| Keywords [eng] |
static analysis ; symbolic execution ; symmetry reduction ; artificial intelligence ; graph neural networks ; quotient state space ; path explosion ; RTOS verification ; formal verification ; program analysis |
| Abstract [eng] |
Symbolic execution of embedded systems faces path explosion, Satisfiability Modulo Theories (SMT) solver bottlenecks, interrupt nondeterminism, and environment modeling complexity. Recent artificial intelligence (AI)-guided approaches using reinforcement learning, graph neural networks, and large language models improve exploration efficiency, yet all reason over raw symbolic states and ignore structural equivalences that arise from symmetry in embedded software. This paper presents S3E, a formal framework that organizes symbolic execution around equivalence classes of states under symmetry transformations. Symmetry groups partition the state space into orbits, and exploration proceeds over canonical representatives within quotient transition systems. Symmetry-aware AI components operate on orbit representatives rather than raw states. Four theoretical results support the framework: orbit preservation, quotient soundness, canonicalization correctness, and constraint reuse correctness. An illustrative case study based on a FreeRTOS-like scheduling environment shows how symmetry reduction collapses equivalent states into orbits, with the potential for reductions that scale factorially with symmetric components. S3E is a theoretical framework; a toy-model prototype validates the core quotient-exploration and constraint-caching mechanis, while empirical evaluation on production firmware remains future work. |
| Published |
Basel : MDPI |
| Type |
Journal article |
| Language |
English |
| Publication date |
2026 |
| CC license |
|
