Inferring Equivalence Classes from Legacy Undocumented Embedded Binaries for ISO 26262-Compliant Testing Marco De Luca
arXiv:2604.22673v1 [cs.SE] 24 Apr 2026
[email protected] University of Naples Federico II Naples, Italy
Domenico Francesco De Angelis [email protected] [email protected] Micron Technology, Inc University of Naples Federico II Naples, Italy
Domenico Amalfitano [email protected] University of Naples Federico II Naples, Italy
Pasquale Cimmino
Anna Rita Fasolino
[email protected] Micron Technology, Inc Naples, Italy
[email protected] University of Naples Federico II Naples, Italy
Abstract
Keywords
Equivalence class partitioning is a well-established test design technique mandated by safety standards such as ISO 26262 for systematic testing of safety software. In industrial practice, however, its application to legacy undocumented embedded firmware is often hindered by incomplete or outdated functional specifications. This paper proposes a binary-level methodology for inferring output-oriented equivalence classes directly from compiled firmware, without relying on source-level annotations or external documentation. The approach combines control-flow reconstruction and guided symbolic execution to analyze individual functions and group execution paths according to indistinguishable observable behavior, including return values and output parameters. An optional post-processing step produces human-readable representations to support comprehension and documentation. The methodology is evaluated in an industrial automotive context through a practitioner-based study assessing correctness and interpretability. Results indicate strong alignment with expert expectations and a positive perception of readability and usefulness for supporting function understanding and test design. These findings demonstrate the feasibility and practical relevance of binarylevel equivalence class inference for systematic testing of legacy undocumented safety embedded software.
Software Architecture Recovery, ISO26262, Reverse Engineering, Embedded Software, Symbolic execution, Equivalence class partitioning
CCS Concepts • Theory of computation → Program semantics; • Software and its engineering → Software reverse engineering; • Social and professional topics → Testing, certification and licensing.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]. EASE ’26, Glasgow, United Kingdom © 2018 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 978-1-4503-XXXX-X/2018/06 https://doi.org/XXXXXXX.XXXXXXX
ACM Reference Format: Marco De Luca, Domenico Francesco, De Angelis, Domenico Amalfitano, Pasquale Cimmino, and Anna Rita Fasolino. 2018. Inferring Equivalence Classes from Legacy Undocumented Embedded Binaries for ISO 26262Compliant Testing. In Proceedings of Make sure to enter the correct conference title from your rights confirmation email (EASE ’26). ACM, New York, NY, USA, 9 pages. https://doi.org/XXXXXXX.XXXXXXX
1
Introduction
Modern automotive embedded systems integrate increasing functionality and performance, leading to rapidly growing software complexity. Safety standards such as ISO 26262 [19] and IEC 61508 [9] therefore prescribe systematic verification processes and recommend black-box test design techniques, including Equivalence Class Partitioning (ECP) [26], to achieve adequate input-domain coverage. In particular, ISO 26262 mandates the use of systematic test design techniques such as ECP for high-ASIL software components (Part 6, Table 8) [17]. In industrial practice, however, applying ECP is often problematic. Automotive software frequently consists of legacy firmware developed without complete or up-to-date functional specifications [23, 24]. Although ISO 26262-8 requires a valid functional specification for software reuse, it allows engineers to assess suitability by analyzing design and implementation artifacts when documentation is incomplete [18]. Consequently, reverse engineering becomes necessary to recover functional behavior and enable systematic test design. These challenges are exacerbated by typical characteristics of industrial firmware, including implicit logic, compiler-specific optimizations, undocumented dependencies, and extensive build-time variability introduced through multilevel build systems and pervasive use of preprocessor directives (e.g., #ifdef). Source-level analyses may therefore produce artifacts that do not correspond to deployed firmware configurations [28]. As confirmed by an internal industrial survey with firmware developers and test engineers, this results in a gap between safety-standard
Marco De Luca, Domenico Francesco De Angelis, Domenico Amalfitano, Pasquale Cimmino, and Anna Rita Fasolino
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
prescriptions and the practical means available for defining and maintaining equivalence classes. Prior work has explored recovering behavioral information without formal specifications through specification mining [4, 11], symbolic execution frameworks such as KLEE, S2E, and ANGR [7, 8, 30], and constraint-based reasoning approaches [3, 33–35]. While effective for invariant detection, test generation, and behavioral modeling, these techniques do not explicitly treat equivalence classes (EC) as first-class testing artifacts nor directly support output-oriented equivalence partitioning as required by equivalence-class-based test design [15]. To address this gap, we introduce an automated technique for inferring ECP directly from compiled binaries of legacy undocumented embedded C software. Operating at the binary level ensures fidelity to deployed configurations and avoids inconsistencies introduced by sourcelevel variability. The approach analyzes executables enriched with DWARF debug information [10], reconstructs control-flow graphs, and performs guided symbolic execution, merging explored paths through constraint-based reasoning to identify inputs that produce indistinguishable observable behavior. We adopt an output-oriented definition of ECs [15], where inputs are equivalent if they induce identical externally observable effects, including return values and state modifications through dereferenced pointer parameters. By grouping symbolic paths that yield the same observable outcomes, the technique recovers undocumented functional boundaries that are difficult to identify manually in legacy undocumented firmware. The main contributions of this paper are: (i) an automated methodology for recovering output-oriented ECs from compiled embedded binaries targeting undocumented or legacy safety software; and (ii) an industrial evaluation assessing their correctness, readability, and usefulness. The remainder of the paper is organized as follows. Section 2 discusses the industrial context; Section 3 presents the methodology; Section 4 provides illustrative examples; Sections 5 report the experimental setup and results; Section 6 presents lessons learned; Section 7 reviews related work; and Section 8 concludes the paper.
2
Industrial Context and Needs Elicitation
The methodology presented in this paper is motivated by challenges observed in an industrial automotive context, where firmware developers and test engineers must design and maintain safety test suites under ISO 26262 constraints. In such environments, equivalence class partitioning is widely recognized as a fundamental test design technique, yet its practical application is often hindered by the lack of reliable specifications and the complexity of legacy undocumented embedded software [12, 18, 24, 27]. To ground the proposed methodology in concrete industrial needs, we asked to conduct a qualitative needs elicitation study based on focus groups, involving twelve practitioners from Micron Technology. Participants included firmware developers and engineers involved in software testing activities, all with experience in safety systems. The focus group was moderated by two of the authors and conducted as a structured discussion session lasting approximately three hours. The discussion addressed three main themes: (i) the role of ECP in safety-oriented test design; (ii) the difficulties of manually defining ECs; and (iii) expectations toward automated support for EC identification and documentation. Notes from the discussion were
analyzed inductively by the authors, following a thematic analysis approach to identify recurring observations and consolidate them into a set of industrial needs relevant to the design of the proposed approach. The outcomes highlight a strong demand for automation. Participants emphasized the importance of function-level ECP for systematic coverage and ISO 26262 compliance, while reporting significant difficulties in manual application due to large input spaces, implicit state-dependent conditions, and the absence of precise expected outputs in legacy firmware. In addition, interpretability emerged as a key requirement: practitioners stressed the need for clear constraints, representative input examples, and traceability to exercised conditions to support test design, review, and maintenance. Overall, these findings reveal a gap between safety-standard requirements and the practical means available for defining and managing EC in legacy embedded software. The identified needs directly motivate the proposed methodology, which focuses on (i) automated derivation of ECs, (ii) an output-oriented notion of equivalence aligned with observable behavior, and (iii) the generation of human-readable representations to support comprehension and reuse in industrial workflows.
3
Proposed Methodology
This section presents the two-phase methodology adopted in this work, which is based on the sequential execution of two phases described in the following. The methodology aims to abstract the functional behavior of individual functions into ECs, defined according to Huang et al. [15], and focuses on computational functions, i.e., functions that do not directly interact with hardware peripherals, interrupts, or timing-dependent I/O, which in industrial practice are typically exercised through integration-level or hardware-inthe-loop testing. The two phases consist of structural analysis and function classification, followed by symbolic execution and EC generation. Phase 1: Structural Analysis and Function Classification. Phase 1 takes as input two build artifacts: the map file and the executable binary in ELF format [32], enriched with debugging information conforming to DWARF [10]. The goal of this phase is to prepare and organize the analysis inputs required for Phase 2 by producing (i) clusters of function control-flow graphs (CFGs) and (ii) serialized debugging information. An overview of the phase is shown in Figure 1. map file (textual)
ELF enrich by DWARF LEGEND ANGR Framework JSON file
map file parser
call-graph
extract CFG
retrieve metrics
CFG
extract debug info
Debug Info
metrics
Grouping into Clusters
Cluster of Function CFGs
Figure 1: Phase 1 overview.
The map file is parsed to recover symbol addresses and crossreferences among compilation units, enabling the reconstruction of inter-function call relationships. From the resulting call graph, two
Inferring Equivalence Classes from Legacy Undocumented Embedded Binaries for ISO 26262-Compliant Testing
metrics are derived for each function to approximate the expected analysis effort: the call depth, which captures the length and complexity of dependency chains, and the number of accessed global variables, which correlates with the size of the symbolic state [14]. In parallel, the ELF binary is analyzed to extract DWARF metadata providing semantically rich information, including function signatures, parameter types, and data-structure definitions. Operating directly on the compiled binary, rather than on source code, preserves fidelity to the deployed configuration and avoids inconsistencies introduced by source-level variability. CFGs for all identified functions are then recovered from the binary using angr. The previously derived call-graph metrics are used to organize these CFGs into clusters, grouping functions with deeper call chains and heavier use of global state. This clustering supports more efficient downstream analysis by reducing execution time and mitigating path explosion and solver load [14]. The outputs of Phase 1 are therefore: (i) a dependency-aware clustering of per-function CFGs guided by call depth and number of accessed global variables, and (ii) a serialized bundle of DWARF-derived debugging information for subsequent phases. Phase 2: Symbolic Execution and ECP Generation. Phase 2 derives a human-readable Equivalence Class Partitioning (ECP) from the clusters of function CFGs and the debugging information produced in Phase 1. An overview of this phase is shown in Figure 2. Debug Info
LEGEND ANGR Framework JSON file
Cluster of Function CFGs
Serialized ECP
LLM-Ready ECP
Selected CFG Generate parameter symbols & constraints symbolic execution
serialization
Merge constraints Constraint simplification path condition
LLM-Ready constraints
Method summary generation & hook
Method summary
LLM post processing
Dataset EC Human Readable
Figure 2: Phase 2 overview.
Clusters are processed in ascending order of call depth and, in case of ties, by increasing number of accessed global variables. This scheduling reduces symbolic execution overhead, as analyzing shallower functions first enables the construction of reusable method summaries [36, 37], which are subsequently reused when exploring deeper call chains. A method summary captures the interface-level behavior of a function by mapping input conditions to observable effects, namely return values and updates to output parameters and global variables. Debug information provides the symbols required for symbolic execution and the initial assumptions over their domains. For each selected function CFG, input parameters are instantiated as symbolic bit-vectors using the angr framework. Type information recovered in Phase 1 is used to constrain symbolic domains, for instance by restricting Boolean parameters to {0, 1}, bounding integer parameters according to their bit width, and limiting enumerated types to their declared constants. For pointer parameters, angr’s clinic mechanism is used to distinguish between scalar objects and arrays, enabling bounded and accurate memory modeling. These constraints substantially reduce infeasible paths and mitigate path explosion. Symbolic execution is then performed
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
under fixed exploration bounds. Loops are unrolled up to 1024 iterations, reflecting bounded patterns commonly observed in industrial embedded firmware, while potentially under-approximating rare corner cases [20, 25]. For each explored path, the analysis collects path conditions and interface-level effects, discards unsatisfiable paths, and normalizes the remaining symbolic states (e.g., last-writewins per location and deterministic ordering of fields and elements). When an output interface yields a symbolic expression 𝑣, the analysis explicitly distinguishes between overflow and non-overflow cases by forking execution into 𝑣 > MAX_VALUE and 𝑣 ≤ MAX_VALUE. To reduce redundancy, loop-derived paths are merged when they traverse the same loop header and exit through identical CFG nodes or edges, yielding possibly disjunctive path conditions. Before equivalence classes are constructed, extracted path conditions undergo a pattern-based simplification step. This step rewrites recurring engine- and compilation-induced idioms into clearer and more conventional forms without altering their semantics. The simplification targets common readability issues, including fragmented byte-wise constraints, redundant Boolean structures, backend-specific operators, and other mechanically generated expressions that obscure the intent of a condition. The applied rewrite patterns are summarized in Table 1 and are used solely as a postprocessing step to facilitate human inspection and documentation [5, 33]. The resulting constraints are semantically equivalent to the original ones and are suitable for subsequent merging and LLM-based post-processing. Equivalence classes are then constructed by merging symbolic states that exhibit identical interface-level behavior. For ECP purposes, paths producing the same return value and the same updates to output parameters and global variables are considered indistinguishable and are represented by a single equivalence class. Each state is characterized by its path condition and an output snapshot summarizing observable effects. Path conditions associated with identical outputs are aggregated via logical disjunction and lightly simplified to improve readability. The merged equivalence classes are consolidated into reusable method summaries [36, 37]. Each summary is serialized as a Python stub compatible with the angr framework and installed through its hooking mechanism. At call sites, the symbolic executor applies the summarized behavior directly, avoiding re-execution of the caller’s internal control flow while preserving its interface-level semantics under the same exploration bounds. This mechanism significantly reduces SMT solving and emulation costs, improving scalability on large industrial firmware. For each analyzed function, the final equivalence classes are serialized into a structured JSON representation that captures both input-domain constraints and corresponding observable outputs, enabling integration into downstream testing and verification workflows. Since symbolic constraints are expressed in low-level bit-vector logic, an optional post-processing step translates them into human-readable descriptions to support practical adoption and manual review for safety certification. An LLM component is used only to improve the human readability of solver-validated symbolic equivalence classes, without affecting symbolic execution, class construction, or analysis decisions. It is guided by a structured prompt that frames the model as a safety engineer and asks it to translate Claripy symbolic constraints
Marco De Luca, Domenico Francesco De Angelis, Domenico Amalfitano, Pasquale Cimmino, and Anna Rita Fasolino
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
Box 1: Role-constrained prompt for EC generation. You are a top-tier ISO 26262 safety-critical engineer. Your task is to convert symbolic constraints (Claripy format) into human-readable equivalence classes. ### Input format ### - Function signature in C. - JSON array of equivalence classes: [{ "__return__": return expression or value, "reference parameters": expression or value, "global variable": expression or value }, "inputs expression representing the equivalence class"] ### Output format ### EC 1: Input ranges in terms of set; Human-readable explanation Constraint equations: <parameter isolated on the left> Example EC 1: Value to trigger this EC 1 EC 2: ... ### Rules ### - Simplify expressions and remove redundancy without changing semantics. - No vector logic in ranges. - Express constraints as equations with one parameter isolated on the left. - One constraints for each function parameter, and not name the return value. - Do NOT infer information not present in the input.
Now process the following input: {function-information}
into human-readable equivalence classes. The prompt combines multiple prompt-engineering techniques from the taxonomy in [29], enforcing a strict input/output structure, semantic preservation, and simplified, non-redundant parameter-isolated constraints with explicit input ranges. The full prompt is reported in Box 1, while the resulting human-readable equivalence classes are stored in the Dataset EC Human Readable file.
4
Examples of Inferred Equivalence Classes
This section presents a set of illustrative examples showing the ECs inferred from legacy embedded software using the proposed methodology. The examples focus on representative function-level patterns commonly observed in industrial automotive firmware, where the absence of precise specifications complicates systematic EC identification. Rather than providing a full end-to-end walkthrough of the analysis workflow, the examples highlight the resulting output-oriented equivalence partitions derived from different control-flow and computation patterns. The examples progressively increase in complexity: Example 1 illustrates conditional branching, Example 2 focuses on loop-induced path clustering, and Example 3 combines arithmetic and bit-level operations. Example 1: Conditional branching. We consider a computational function extracted from the executable binary that assigns a value to an output parameter based on a single input variable. The function contains a sequence of conditional branches that partition the input domain into distinct regions, making it a representative example to illustrate output-oriented EC extraction. Figure 3 shows, from left to right, the source code of the function, the reconstructed control-flow graph (CFG), and the symbolic constraints derived from path exploration. While these constraints precisely capture the branching logic, they are expressed in a low-level symbolic form and are not directly suitable for test design. By grouping paths that induce identical observable effects on the output parameter pout, the methodology derives a compact set of ECs that preserve the original semantics while substantially improving readability. The inferred ECs are post-processed into a human-readable description to support communication and review
void f1(uint16_t pin, uint8_t* pout) { // N0 if (pin >= 0x541) // N1 *pout = 1; // N2 else if ((pin >= 0x21C) \ && (pin <= 0x2B0)) // N3 *pout = 2; //N4 else *pout = 3; //N5 } // N6
N0
S0
N1 N2
N3 N4
pin >= 0x541
S1
T
F
S2 pout=1 N5
T
(pin >= 0x21C) && S3 (pin <= 0x2B0) F
S4 pout=2
N6
S5 pout=3
S6
Figure 3: Code, CFG, and symbolic path conditions of f1
by test engineers. The resulting ECs and their corresponding input conditions are reported in Table 2. Table 2: ECs derived for f1. EC ID return value pout
ECP
LLM Output
EC_1
none
1
0x540 < pin
pin in {0x0540, ..., 0xFFFF}; for any pout pointer, the function writes 1 to *pout. Constraint equations: pin >= 0x540 Example EC 1: pin = 0x541
EC_2
none
2
0x21C ≤ pin ∧ pin ≤ 0x2B0
pin in {0x021C, ..., 0x02B0}; for any pout pointer, the function writes 2 to *pout. Constraint equations: (pin > 0x21B AND pin <= 0x2B0) Example EC 2: pin = 0x021C
EC_3
none
3
pin < 0x21C ∨ ( pin > 0x2B0 ∧ pin ≤ 0x540 )
pin in {0x0000, ..., 0x021B} U {0x2B1, ..., 0x0540}; for any pout pointer, the function writes 3 to *pout. Constraint equations: pin <= 0x21B OR (pin > 0x2B0 AND pin <= 0x540) Example EC 3: pin = 0x0000 (first range) or pin = 0x2B1 (second range)
Example 2: Loop-induced path clustering. This example considers a function whose control flow is dominated by a loop. The function f2 iteratively inspects the bits of its input parameter and returns either the index of the first set bit or a sentinel value when no such bit is found. Symbolic execution generates multiple execution paths corresponding to different loop iterations. Although these paths differ in the number of iterations, they represent only two distinct observable behaviors: the presence or absence of at least one set bit. Figure 4 illustrates the function source code, the reconstructed control-flow graph (CFG), and the symbolic constraints obtained from path exploration. By grouping loop-exiting paths with identiN0 uint8_t f2(uint8_t p1) { // N0 for (uint8_t i = 0u; i < 8u; i++) // N1 { if (p1 & (1u << i)) // N2 return i; //N3 } // N4 return 0xFFu; // N5 }
S0 p1 & (1<<0)
N1 T N2
N3
S1
S2 return 0 N4
F
p1 & (1<<1)
S3 F
T
F p1 & (1<<1)
T
S4 return 1
T S14
N5
return 7
S3
F S15 return 0xFF
Figure 4: Code, CFG, and symbolic path conditions of f2
cal observable outcomes, the method collapses all return-to-loop paths into a single EC while retaining a distinct class for the case where no bit is set. A final LLM post-processing step is then applied, as shown in Table 3. Table 3: ECs derived for f2. EC ID
return value
ECP
LLM Output
p1 = 0; when p1 = 0, the function returns 0xFF. EC_1 0xFF p1 == 0 Constraint equations: p1 = 0 Example: p1 = 0 p1 in {1, ..., 255}; when p1 != 0, the function returns a value in the range 0 ... 7 (inclusive). EC_2 0 ≤ ret < 8 p1 ≠ 0 Constraint equations: p1 != 0 Example: p1 = 1
Example 3: Arithmetic and bit-level constraints. This example illustrates equivalence class extraction for a function that combines
Inferring Equivalence Classes from Legacy Undocumented Embedded Binaries for ISO 26262-Compliant Testing
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
Table 1: Rules for constraint simplification. ID Description
Ref
1
[5]
2 3 4 5 6 7 8
When a fixed-size value is constrained by specifying constant values for individual slices, combine those slice-by-slice constraints into a single constraint on the whole value, and present the resulting constant as a signed integer (two’s complement). Simplify Boolean expressions by eliminating redundant negations/conditions, applying standard logical rewrites, and compacting overlapping comparisons on the same constant into a stronger, shorter predicate Simplify arithmetic expressions by factoring out common multiplicative terms, reducing repetition. Rewrite engine-specific comparison functions into their equivalent standard math comparisons to improve readability. Detect the verbose bit-by-bit disjunction expression that encodes “at least one bit is set” and replace it with the equivalent non-zero check. Rewrite “append 𝑘 zeros to 𝑥” concatenations as a left shift 𝑥 ≪ 𝑘 to obtain a more familiar form. Rewrite comparisons on left-shifted values into equivalent comparisons on the unshifted variable, adjusting the constant accordingly. Rewrite conditional (if–then–else) expressions (contained in path condition) into separate cases, one per branch guard, and treat each case as a distinct equivalence class partition
[33] [33] [33] proposed proposed proposed proposed
proposed = Rule proposed and implemented for this methodology.
arithmetic operations with bit-level manipulation of multiple input parameters. The function f3 extracts bit fields from its inputs, applies conditional arithmetic based on a boolean flag, and reconstructs the output value. Different combinations of the boolean flag and arithmetic outcomes give rise to multiple execution paths that, while syntactically distinct, can be grouped according to their observable effects on the returned value. Figure 5 shows the function source code, the reconstructed control-flow graph (CFG), and the symbolic constraints derived from path exploration.
uint32_t f3(uint32_t p1, uint32_t p2, bool p3) { // N0 uint32_t x = p1; // N1 uint32_t y = (p1 >> 20) & 511u; // N2 uint32_t z = p1 & 0xFFFFFu; // N3 z = (p3 == true) ? z+p2 : z-p2; // N4 - N5 return (y << 20u) + z; //N6 }
N0
N0
N1
N1
N2
N2 p3 == true
N3 N4
T N5
N3
N4 z = z+p2
N5
F N5 z = z-p2
N5
Figure 5: Source code, CFG, and symbolic constraints for f3.
Grouping paths with identical interface outputs produces a compact set of ECs encompassing both arithmetic and bit-level constraints. A post-processing step then generates human-readable descriptions, as reported in Table 4. Table 4: ECs derived for f3. EC ID
return value
EC_1
p2 + p1[19:0] + (p1[28:20]..0x0)
EC_2
p1[19:0] - p2 + (p1[28:20]..0x0)
EC_3
p1[19:0] - p2 + (p1[28:20]..0x0)
5
ECP
LLM Output
Input ranges: {p3 = 1; p2 in [0, 0xFFFFFFFF]; p1 in [0, 0xFFFFFFFF]} Addition path without overflow - the function computes p1 + (p2 & 0xFFFFF) + (((p2 >> 20) & 0x1FF) << 4) and the sum fits in 32 bits. p3 == 1 AND p2 + p1[19:0] + Constraint equations: (p1[28:20]..0x0) <= 0xFFFFFFF p2 in [0, 0xFFFFFFFF] p1 <= 0xFFFFFFFF - ((p2 & 0xFFFFF) + (((p2 >> 20) & 0x1FF) << 4)) Example : p3 = 1, p2 = 0xFFFFFFFF, p1 = 0 Input ranges: {p3 = 0; p2 in [0, 0xFFFFFFFF]; p1 in [0, 0xFFFFFFFF]} Subtraction path without overflow - the function computes (p2 & 0xFFFFF) - p1 + (((p2 >> 20) & 0x1FF) << 4) and the result is <= 0xFFFFFFFF. p3 == 0 AND p1[19:0] - p2 + Constraint equations (p1[28:20]..0x0) <= 0xFFFFFFF p2 in [0, 0xFFFFFFFF] p1 >= ((p2 & 0xFFFFF) + (((p2 >> 20) & 0x1FF) << 4)) - 0xFFFFFFFF Example: p3 = 0, p2 = 0x00010000, p1 = 0 Input ranges: {p3 = 0; p2 in [0, 0xFFFFFFFF]; p1 in [0, 0xFFFFFFFF]} Addition path with overflow: p1 + (p2 & 0xFFFFF) + (((p2 >> 20) & 0x1FF) << 4) exceeds 32-bit maximum (> 0xFFFFFFFF). p3 == 0 AND p1[19:0] - p2 + Constraint equations: (p1[28:20]..0x0) > 0xFFFFFFFF p2 in [0, 0xFFFFFFFF] p1 > 0xFFFFFFFF - ((p2 & 0xFFFFF) + (((p2 >> 20) & 0x1FF) << 4)) Example: p3 = 1, p2 = 0xFFFFFFFF, p1 = 0xFFFFFFFF
Experimental Evaluation
This section presents the industrial validation grounded in the needs identified in Section 2, in particular the lack of systematic support for equivalence class partitioning on legacy firmware and
the difficulties of interpreting low-level symbolic constraints. To address these challenges, we conducted a practitioner-centered study involving firmware developers and test engineers, structured to minimize bias and to reflect realistic automotive testing workflows. Rather than benchmarking the proposed methodology against existing academic techniques, the evaluation focuses on whether the generated equivalence classes are considered correct, usable, and readable by practitioners in real-world automotive firmware testing scenarios. Given the absence of authoritative functional specifications for legacy binaries, correctness is operationalized as agreement with expert-derived expectations of functional behavior. Readability and usability are evaluated separately, with particular attention to the added value of human-readable representations. The validation is organized around the following research questions: • RQ1: To what extent do the equivalence classes generated by the tool agree with expert-derived expectations of functional behavior? Rationale: This question assesses the accuracy of the automated extraction by comparing tool-generated partitions against expert expectations in the absence of authoritative specifications. • RQ2: To what extent are the generated equivalence classes human-readable and interpretable by firmware engineers? Rationale: This question evaluates usability by examining whether the inferred classes are readable and suitable for practical test design and review in industrial settings. The research questions are addressed using survey-based metrics. Functional correctness, information adequacy, readability, interpretability, and usability are measured through Likert-scale items, while perceived usefulness and missing information are captured through multiple-choice frequency counts. This combination allows both quantitative aggregation and diagnostic insight into practitioners’ perceptions of the generated equivalence classes. The objects of the evaluation are computational functions extracted from industrial automotive firmware binaries. We selected functions implementing pure logic, without direct interaction with peripherals, interrupts, or timing-dependent I/O, and exposing explicit inputs and observable outputs, thus enabling output-oriented equivalence class partitioning. Overall, we considered 27 functions, with line of code metrics in average 31 LOC. for which the tool generated 138 equivalence classes, with a median of 15 and average of 21 classes per function. These study objects reflect the class of legacy firmware
Marco De Luca, Domenico Francesco De Angelis, Domenico Amalfitano, Pasquale Cimmino, and Anna Rita Fasolino
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
components for which practitioners reported the strongest need for systematic equivalence partitioning support (Section 2). The participants were recruited from the same cohort involved in the preliminary needs assessment described in Section 2. This choice ensured continuity between the industrial needs elicited in the first study and the subsequent validation of the proposed approach, enabling participants to assess the tool outputs against challenges they had previously reported in their daily work. To address the research questions, we designed a questionnaire combining closed-ended items measured on a 5-point Likert scale with multiple-choice questions aimed at collecting categorical and diagnostic feedback. The latter also includes an optional open-ended field for additional comments. Table 5 reports the complete questionnaire together with the mapping of items to the corresponding research questions, while the predefined response options for the multiple-choice items are summarized in Table 6. The questionnaire is organized into two sections aligned with the two research questions: the first focuses on functional correctness and information adequacy, while the second evaluates readability, interpretability, and perceived utility within typical engineering workflows. During execution and analysis, participants performed a structured evaluation task designed to reflect common testing activities on legacy and undocumented firmware. For each target function, they first analyzed the source code independently and derived equivalence classes according to their usual testing practices, without access to any tool-generated artifacts. They were then presented with the equivalence classes generated by the proposed tool and asked to compare them with their manually derived ones, assessing alignment, completeness, and potential discrepancies. Upon completing this comparison, participants filled in the questionnaire capturing their subjective assessment of the tool-generated artifacts. Survey responses were collected anonymously and analyzed using descriptive statistics. Likert-scale items were aggregated after normalizing reverse-coded questions, while multiple-choice items were analyzed using frequency-based aggregation to synthesize practitioners’ judgments across the considered dimensions.
5.1
Answer to RQ1
Figure 6 reports the distribution of responses to Q1–Q3, showing an overall positive assessment of the generated equivalence classes in terms of functional correctness and information adequacy. For Q1, which evaluates alignment with expected functional behavior, all responses were positive or neutral, with a clear prevalence of Agree and Strongly Agree, indicating strong consistency between tool-generated results and expert expectations. A similar pattern is observed for Q2, where most respondents expressed agreement, with a limited number of neutral responses, suggesting minor concerns about missing information. Responses to Q3 remain broadly positive, although with slightly higher neutrality, indicating that some participants perceived room for reducing unnecessary detail while still considering the information accurate and appropriate. Table 6 summarizes responses to Q4. Boundary conditions were the most frequently reported missing aspect, followed by path feasibility details, while missing constraints on symbolic variables were rarely indicated. Notably, several participants reported no missing information. Overall, the identified gaps mainly concern edge-case
Q1 Q2 Q3
2 (17%) 3 (25%) 4 (33%) SD (1)
5 (42%)
6 (50%)
5 (42%) 7 (58%)
3 (25%)
1 (8%) D (2) N (3) A (4) SA (5) Figure 6: Likert-scale rating distribution for Q1, Q2, Q3
characterization and path feasibility, rather than the core functional behavior captured by the inferred equivalence classes. RQ1 Answer The inferred equivalence classes largely align with expert expectations of functional behavior. Participants reported high perceived correctness, with only minor gaps related to boundary conditions and path feasibility. Overall, the results indicate that the approach produces accurate and sufficiently informative equivalence classes for understanding function behavior.
5.2
Answer to RQ2
Figure 7 reports responses to Q5, Q8, and Q9, showing a generally positive perception of the generated equivalence classes in terms of readability, interpretability, and usability. Most respondents expressed agreement that the equivalence classes are human-readable and interpretable (Q5), with a limited number of neutral responses indicating minor room for improvement. An even stronger consensus emerges for Q8 and Q9, where the large majority of participants agreed that the approach supports understanding of function behavior and is usable within typical engineering workflows. 3 6 3 Q5 (25%) (50%) (25%) 1 9 2 Q8 (8%) (75%) (17%) 2 6 4 Q9 (17%) (50%) (33%) SD (1) D (2) N (3) A (4) SA (5) Figure 7: Likert-scale rating distribution for Q5, Q8, Q9
Table 6 summarizes responses to the multiple-choice questions. For Q6, equivalence class sets and simplified constraints were most frequently selected, indicating a clear preference for compact, highlevel representations, while branch-specific versions were selected less often. Responses to Q7 further confirm this trend: most participants reported that the generated equivalence classes enhance understanding compared to manual analysis, with only a small minority indicating that they contain excessive information. RQ2 Answer The inferred equivalence classes are perceived as readable, interpretable, and usable by firmware engineers. Participants reported that the approach supports understanding of function behavior, with clear preference for compact outputs (e.g., equivalence class sets, simplified constraints). Overall, results indicate improved comprehension without introducing excessive information.
5.3
Threats to Validity
This study proposes an automated methodology for inferring output-oriented equivalence classes from legacy embedded binaries and evaluates its perceived correctness and usability through an industrial practitioner survey. The main threats to validity and corresponding mitigations are discussed below. Construct validity. The correctness of inferred equivalence classes cannot be assessed against complete formal specifications, as the
Inferring Equivalence Classes from Legacy Undocumented Embedded Binaries for ISO 26262-Compliant Testing
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
Table 5: Questionnaire items and their mapping to the research questions. ID Question Question semantic Part 1 - RQ1 Q1 The produced equivalence classes correctly match the expected functional behavior Functional correctness Q2 The produced equivalence classes miss important information, which can make understanding the function Information adequacy behavior difficult Q3 The produced equivalence classes contain unnecessary information Information adequacy Q4 If there is missing information in the equivalence classes, which kind is it? Information adequacy Part 2 – RQ2 Q5 The produced equivalence classes are human-readable and interpretable Readability & Interpretability Q6 Which outputs produced by the method do you find useful for understanding the function? Practical utility and Usability Q7 Based on your experience, please indicate which of the following statements you believe to be true. Practical utility and Usability Q8 Based on my experience in using the method, I find it useful in supporting function behavior comprehension. Practical utility and Usability Q9 Based on my experience, I am satisfied with the usability of the method. Practical utility and Usability L = 5-point Likert scale; MC = Multiple choice. Table 6: Multiple-choice response options and responses. Q4
□ Constraints on symbolic variables. □ Boundary conditions. □ Path feasibility details. □ Free text for other options.
Votes 1 6 4 3
Q6
□ Equivalence class sets. □ Simplified constraints. □ Branch-specific versions. □ Free text for other options.
8 7 4 3
Q7
□ Compared to manual analysis, the automatically derived equivalence classes enhance understanding. □ Compared to manual analysis, the automatically derived equivalence classes contain too much information that can interfere with understanding. □ Manual and automatic approaches provide similar information. □ Free text for other options.
10 2 0 0
analyzed firmware consists of legacy assets with partially missing or outdated documentation. Practitioners’ judgments are therefore used as a proxy for functional correctness, introducing an inherent degree of subjectivity. To mitigate anchoring effects, the survey adopted a two-phase structure in which participants first analyzed function behavior independently and only then inspected the generated artifacts. Usability and interpretability are assessed through Likert-scale responses and thus reflect perceived utility rather than objective improvements in testing effectiveness. Internal validity. The methodology relies on the availability and quality of binary metadata (e.g., DWARF information, map files) to recover function interfaces and control-flow structure. Inaccurate or incomplete metadata may affect constraint reconstruction and, consequently, equivalence class inference. In addition, symbolic execution is sensitive to modeling assumptions and exploration bounds. The implementation adopts constraints typical of safety-critical embedded software (e.g., no recursion, no dynamic memory allocation, bounded loops); deviations from these assumptions or path explosion may result in missed or imprecise behaviors. Since equivalence classes are defined with respect to observable outputs, unmodeled side effects (e.g., hardware interactions, timing-dependent behavior) are not captured. An optional LLM-based post-processing step is used exclusively to transform already-derived constraints into human-readable form. While it does not affect the symbolic analysis, it may influence perceived readability and is therefore treated strictly as a presentation layer. External validity. External validity is limited by both the study objects and the participant sample. Although the relatively small set of analyzed functions may affect generalizability, the methodology has
Type L L L MC L MC MC L L
been applied in production environments to a significantly larger corpus of industrial functions. The selected subset was chosen to ensure a manageable workload for practitioners during manual review. The consistent behavior observed across the wider (undisclosed) codebase provides additional confidence in the scalability and robustness of the approach. Furthermore, the evaluation focuses on computational functions extracted from automotive firmware developed under ISO 26262 constraints and involves a convenience sample from a single organization. As a result, the findings may not generalize to other domains, binary characteristics, or development practices. However, this scope reflects the intended industrial context and aligns with the standard constraints of safety-critical embedded software development.
6
Lessons Learned from Industrial Adoption
This section discusses lessons learned from the industrial application of the proposed approach, drawing on the experimental evaluation and practitioner feedback. No new empirical evidence is introduced. Given the limited sample size (n=12) and single-organization context, the findings should be interpreted with caution in terms of external validity and generalizability. LL1: Readability is a prerequisite for usability. Although the quantitative results indicate a generally positive perception of readability and interpretability (RQ2), practitioners emphasized that relatively minor presentation choices can significantly affect practical usability. Qualitative feedback highlighted formatting aspects and naming practices, noting that “better indentation would increase readability” and that “where possible, numeric literals should be replaced with C macros or named constants.” These observations suggest that, in industrial settings, equivalence classes are treated as engineering artifacts to be inspected, reviewed, and potentially maintained, rather than as purely analytical outputs. A key lesson is therefore the importance of sensible default formatting (e.g., consistent indentation, whitespace, and visual grouping) and the systematic use of named constants instead of magic numbers, supported by lightweight annotations to convey semantics. LL2: Human-readable and machine-readable outputs serve complementary roles. While readability was repeatedly identified as essential for manual inspection and review, the results also indicate that practitioners value representations that strike a balance between human interpretability and the ability to be
Marco De Luca, Domenico Francesco De Angelis, Domenico Amalfitano, Pasquale Cimmino, and Anna Rita Fasolino
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
systematically processed, reused, and integrated into existing industrial workflows. In practice, equivalence classes may thus serve a dual role: supporting human understanding of functional behavior and acting as structured artifacts that enable traceability, automation, and downstream analyses within the development and testing toolchain, particularly in safety-critical contexts where reviewability and traceability are required by standards. This dual role is further reinforced by unsolicited practitioner comments collected outside the survey, including the preference to “prefer a structured JSON output, even if it is harder to read.” Rather than contradicting the emphasis on readability, this feedback highlights the need to balance human interpretability with structural rigor. A practical implication is to support both consumption modes by providing dual outputs: a machine-readable representation suitable for automation and validation, and a concise human-readable summary tailored to review and comprehension tasks. Overall, these lessons indicate that relatively modest refinements in presentation and output structuring can substantially improve the perceived usability and integration potential of automatically inferred equivalence classes in industrial contexts. At the same time, the findings reinforce that adoption in safety-critical workflows depends not only on analytical correctness but also on predictability, readability, and compatibility with existing toolchains. While preliminary, these insights provide concrete guidance for refining the approach and motivate future studies involving broader populations, multiple projects, and longitudinal evaluations.
7
Related Studies
This section briefly reviews existing work on equivalence class partitioning and related specification inference techniques, highlighting their limitations in the context of legacy embedded software. Equivalence Class Partitioning (ECP) is a classical black-box test design technique in which the input domain is divided into subsets expected to exhibit uniform behavior. Traditional manual ECP relies on functional specifications, domain knowledge, and heuristics, often combined with Boundary Value Analysis. While effective in well-specified systems, this approach requires substantial human effort and assumes explicit knowledge of input constraints, which is rarely available for large-scale or legacy embedded software. To reduce manual effort, model-based approaches automate equivalence class extraction from formal behavioral models such as state machines or transition systems. For example, Hübner et al. [16] propose a strategy that is complete with respect to a given fault model and supports infinite input domains. However, these techniques critically depend on the availability and correctness of manually constructed models, which are often unavailable or costly to maintain in industrial embedded contexts. A large body of work on specification mining aims to infer behavioral properties from source code or execution traces to support program comprehension, test generation, and verification. Usage pattern mining techniques capture frequent API call co-occurrences or ordering constraints [6], while static and symbolic analyses infer invariants and path conditions through control-flow, data-flow, or symbolic execution. Although symbolic execution enables precise constraint extraction and has been used to recover high-level semantics from binaries [21, 22, 31], existing tools such as DisPatch [22], REMaQE [33], and PERFUME [34] primarily
target program understanding or reverse engineering, rather than test-oriented equivalence class extraction. Declarative approaches based on Constraint Logic Programming (CLP) integrate symbolic execution and constraint solving into the execution semantics, enabling systematic path exploration and test case generation [1, 2, 13]. While expressive and compositional, these approaches typically do not treat equivalence classes as first-class testing artifacts and are rarely applied directly to industrial embedded binaries. Overall, existing approaches exhibit complementary strengths but also limitations that hinder their adoption for equivalence-class-based testing of legacy embedded software. Manual and model-based techniques rely on specifications or models that are often missing in practice, while specification mining and symbolic execution approaches usually treat equivalence classes as a by-product rather than as a primary testing abstraction. The approach proposed in this paper addresses these limitations by directly inferring outputoriented equivalence classes from compiled embedded binaries. By leveraging symbolic execution and constraint merging at the binary level, the method derives compact, test-relevant equivalence partitions without requiring explicit specifications or manually constructed models, aligning symbolic analysis techniques with the practical needs of ISO 26262-compliant testing in industrial settings.
8
Conclusions and Future Work
This paper presented a binary-level methodology for inferring equivalence classes from legacy embedded firmware in the absence of reliable functional specifications. The approach targets a common but underexplored industrial scenario in safety domains, where test design techniques are recommended by standards such as ISO 26262. By operating directly on compiled binaries and combining control-flow reconstruction with guided symbolic execution, the method aligns the extracted equivalence classes with the actual deployed firmware configuration. A central contribution of this work is the treatment of equivalence classes as first-class testing artifacts derived from observable functional behavior. By grouping symbolic execution paths according to equivalent outputs, the approach yields equivalence partitions that support systematic test design rather than merely exposing low-level path conditions. Scalability and industrial feasibility are supported through dependencyaware analysis, bounded symbolic execution, and reusable function summaries, while optional post-processing improves readability without altering the analysis. The industrial evaluation provides preliminary evidence that the inferred equivalence classes align with expert expectations and are considered readable and useful for understanding function behavior and supporting test design in legacy systems. Although the study does not aim at statistical generalization, the results suggest that binary-level equivalence class extraction can effectively complement manual testing in safetycritical industrial contexts. Future work will focus on extending the approach to broader execution environments and language features, as well as on integrating the extracted equivalence classes into downstream test generation and coverage assessment workflows. Additional empirical studies on larger and more diverse industrial codebases are planned to further assess scalability and practical impact.
Inferring Equivalence Classes from Legacy Undocumented Embedded Binaries for ISO 26262-Compliant Testing
References [1] Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, and Jose Miguel Rojas. 2014. Test Case Generation by Symbolic Execution: Basic Concepts, a CLP-Based Instance, and Actor-Based Concurrency. Springer International Publishing, Cham, 263–309. doi:10.1007/978-3-319-07317-0_7 [2] ELVIRA ALBERT, MARÍA GARCÍA DE LA BANDA, MIGUEL GÓMEZZAMALLOA, JOSÉ MIGUEL ROJAS, and PETER STUCKEY. 2013. A CLP heap solver for test case generation. Theory and Practice of Logic Programming 13, 4–5 (2013), 721–735. doi:10.1017/S1471068413000458 [3] Roberto Amadini, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2019. Constraint Programming for Dynamic Symbolic Execution of JavaScript. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research, Louis-Martin Rousseau and Kostas Stergiou (Eds.). Springer International Publishing, Cham, 1–19. [4] Glenn Ammons, Rastislav Bodík, and James R. Larus. 2002. Mining specifications. SIGPLAN Not. 37, 1 (Jan. 2002), 4–16. doi:10.1145/565816.503275 [5] Tod Tracy Amon and Timothy James Loffredo. 2020. Creating Human Readable Path Constraints from Symbolic Execution. Technical Report. Sandia National Lab.(SNL-NM), Albuquerque, NM (United States). [6] Saswat Anand, Edmund K. Burke, Tsong Yueh Chen, John Clark, Myra B. Cohen, Wolfgang Grieskamp, Mark Harman, Mary Jean Harrold, Phil McMinn, Antonia Bertolino, J. Jenny Li, and Hong Zhu. 2013. An orchestrated survey of methodologies for automated software test case generation. Journal of Systems and Software 86, 8 (2013), 1978–2001. doi:10.1016/j.jss.2013.02.061 [7] Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs.. In OSDI, Vol. 8. 209–224. [8] Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2011. S2E: A platform for in-vivo multi-path analysis of software systems. Acm Sigplan Notices 46, 3 (2011), 265–278. [9] International Electrotechnical Commission. 2010. Functional safety of electrical/electronic/programmable electronic safety-related systems. [10] DWARF Debugging Information Format Committee. 2017. DWARF Debugging Information Format Version 5. DWARF Committee. https://dwarfstd.org/doc/ DWARF5.pdf Available under the GNU Free Documentation License, Version 1.3. [11] Yiming Fan and Meng Wang. 2024. Specification mining based on the ordering points to identify the clustering structure clustering algorithm and model checking. Algorithms 17, 1 (2024), 28. [12] Vahid Garousi, Michael Felderer, Çağrı Murat Karapıçak, and Uğur Yılmaz. 2018. Testing embedded software: A survey of the literature. Information and Software Technology 104 (2018), 14–45. doi:10.1016/j.infsof.2018.06.016 [13] MIGUEL GÓMEZ-ZAMALLOA, ELVIRA ALBERT, and GERMÁN PUEBLA. 2010. Test case generation for object-oriented imperative languages in CLP. Theory and Practice of Logic Programming 10, 4–6 (2010), 659–674. doi:10.1017/ S1471068410000347 [14] Gábor Horváth, Réka Kovács, and Zoltán Porkoláb. 2024. Scaling Symbolic Execution to Large Software Systems. ArXiv abs/2408.01909 (2024). https: //api.semanticscholar.org/CorpusID:271709984 [15] Wen-Ling Huang and Jan Peleska. 2016. Complete model-based equivalence class testing. Int. J. Softw. Tools Technol. Transf. 18, 3 (2016), 265–283. doi:10.1007/ s10009-014-0356-8 [16] Felix Hübner, Wen ling Huang, and Jan Peleska. 2015. Experimental Evaluation of a Novel Equivalence Class Partition Testing Strategy. In Tests and Proofs (TAP 2015) (Lecture Notes in Computer Science, Vol. 9154). Springer, 155–172. doi:10.1007/978-3-319-21215-9_10 [17] ISO. 2018. ISO 26262 — Road vehicles — Functional safety — Part 6: Product development at the software level. [18] ISO. 2018. ISO 26262 — Road vehicles — Functional safety — Part 8: Supporting processes. [19] ISO/TC 22/SC 32. 2018. Road vehicles – Functional safety – Part 1: Vocabulary. Standard ISO 26262-1:2018 to ISO 26262-12:2018. International Organization for Standardization, Geneva, Switzerland. https://www.iso.org/standard/68383.html [20] Joxan Jaffar, Jorge A Navas, and Andrew E Santosa. 2011. Unbounded symbolic execution for program verification. In International Conference on Runtime
EASE ’26, June 09–12, 2026, Glasgow, United Kingdom
Verification. Springer, 396–411. [21] Anastasis Keliris and Michail Maniatakos. 2018. ICSREF: A framework for automated reverse engineering of industrial control systems binaries. arXiv preprint arXiv:1812.03478 (2018). [22] Taegyu Kim, Aolin Ding, Sriharsha Etigowni, Pengfei Sun, Jizhou Chen, Luis Garcia, Saman Zonouz, Dongyan Xu, and Dave Tian. 2022. Reverse engineering and retrofitting robotic aerial vehicle control firmware using dispatch. In Proceedings of the 20th Annual International Conference on Mobile Systems, Applications and Services. 69–83. [23] David Lo, {Siau Cheng} Khoo, Chao Liu, and Jiawei Han. 2011. Specification mining: A concise introduction. CRC Press, 1–27. Publisher Copyright: © 2011 by Taylor & Francis Group, LLC.. [24] Srinivas Malladi, G. Ramakrishna, K. Rao, and E Babu. 2016. Analysis of Legacy System in Software Application Development: A Comparative Survey. International Journal of Electrical and Computer Engineering (IJECE) 6 (02 2016), 292–297. doi:10.11591/ijece.v6i1.8367 [25] Bertrand Meyer. 2024. A formal definition of loop unrolling with applications to test coverage. arXiv preprint arXiv:2403.08923 (2024). [26] Glenford J Myers, Tom Badgett, Todd M Thomas, and Corey Sandler. 2004. The art of software testing. Vol. 2. Wiley Online Library. Automating Requirements-Based Testing for ISO [27] QA Systems. 2020. 26262. https://www.qa-systems.com/wp-content/uploads/2020/12/automatingrequirements-based-testing-for-iso-26262.pdf. [28] Abdullah Qasem, Paria Shirani, Mourad Debbabi, Lingyu Wang, Bernard Lebel, and Basile L. Agba. 2018. Automatic Vulnerability Detection in Embedded Device Firmware and Binary Code: Survey and Layered Taxonomies. ACM Computing Surveys — Extended Version 1, 1 (2018), 1–40. doi:10.1145/1122445.1122456 [29] Yuya Sasaki, Hironori Washizaki, Jialong Li, Nobukazu Yoshioka, Naoyasu Ubayashi, and Yoshiaki Fukazawa. 2025. Landscape and Taxonomy of Prompt Engineering Patterns in Software Engineering. IT Professional 27, 1 (2025), 41–49. doi:10.1109/MITP.2024.3525458 [30] Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Audrey Dutcher, Jessie Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. 2016. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. (2016). [31] Pengfei Sun, Luis Garcia, and Saman Zonouz. 2019. Tell me more than just assembly! reversing cyber-physical execution semantics of embedded iot controller software binaries. In 2019 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, 349–361. [32] Tool Interface Standards (TIS) Committee 1995. Tool Interface Standard (TIS) Executable and Linking Format (ELF) Specification. Tool Interface Standards (TIS) Committee. https://refspecs.linuxfoundation.org/elf/elf.pdf Accessed: 2026-01-20. [33] Meet Udeshi, Prashanth Krishnamurthy, Hammond Pearce, Ramesh Karri, and Farshad Khorrami. 2024. REMaQE: Reverse Engineering Math Equations from Executables. ACM Trans. Cyber-Phys. Syst. 8, 4, Article 43 (Nov. 2024), 25 pages. doi:10.1145/3699674 [34] Nicolaas Weideman, Virginia K Felkner, Wei-Cheng Wu, Jonathan May, Christophe Hauser, and Luis Garcia. 2021. Perfume: Programmatic extraction and refinement for usability of mathematical expression. In Proceedings of the 2021 Research on offensive and defensive techniques in the Context of Man At The End (MATE) Attacks. 59–69. [35] Hendrik Winkelmann, Jan C. Dageförde, and Herbert Kuchen. 2021. ConstraintLogic Object-Oriented Programming with Free Arrays. In Functional and Constraint Logic Programming, Michael Hanus and Claudio Sacerdoti Coen (Eds.). Springer International Publishing, Cham, 129–144. [36] Qiuping Yi, Junye Wen, and Guowei Yang. 2020. Summary-guided incremental symbolic execution. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Companion Proceedings. 310–311. [37] Yicheng Zeng, Jiaqian Peng, Jiami Lin, Rongrong Xi, and Hongsong Zhu. 2024. Symerge: Replacing Calls in Under-Constrained Symbolic Execution and Find Vulnerabilities. In Security and Privacy in Communication Networks, Saed Alrabaee, Kim-Kwang Raymond Choo, Ernesto Damiani, and Robert H. Deng (Eds.). Springer Nature Switzerland, Cham, 376–399.