In the context of formal methods, symbolic execution stands out as highly automatic, allowing static code analysis to be adopted by users without domain specific expertise or training.

Symex is a symbolic execution framework specifically targeting analysis of embedded software with requirements to safety, security, and dependability. However, so far, the execution engine of Symex has been executing LLVM-IR. Because no consistent mapping between LLVM-IR and actual machine code exists, Symex has been unable to provide guarantees to runtime properties of the system, such as Worst-Case Execution Time (WCET).

In this paper, we extend Symex by moving the execution engine to \textit{General Assembly} (GA), an Intermediate Representation (IR) capable of capturing the semantics of commonplace Instruction Set Architectures (ISAs), along with their non-functional properties, e.g. per-instruction execution time, or power consumption. Symex lifts the ELF binary to GA and explores all reachable paths without approximations, thus it is able to provide guarantees to runtime characteristics of the system, taking into account architecture specific behaviour and compiler backend/linker optimizations.

Furthermore, we introduce the EASY system analysis framework, which uses Symex as a symbolic execution backend, and therefore grants the same verification capabilities. EASY can provide analysis for response time, task memory isolation and application stack memory utilization.

We demonstrate the feasibility of GA-based symbolic execution by modelling the full ARMv6 and most of the v7 ISA, as well as the RV32I ISA. Leveraging on the Rust RTIC framework, we demonstrate that EASY is capable of automatically determining the schedulability, worst-case stack memory utilization and task memory isolation properties of the system.