US Patent 9536093 Automated verification of a software system

Software code of a software system (e.g., a software stack) may be verified as conforming to a specification. A high-level language implementation of the software system may be compiled using a compiler to create an assembly language implementation. A high-level specification corresponding to the software system may be translated to a low-level specification. A verifier may verify that the assembly language implementation functionally conforms to properties described in the low-level specification. In this way, the software system (e.g., a complete software system that includes an operating system, device driver(s), a software library, and one or more applications) may be verified at a low level (e.g., assembly language level).