Automated Verification of a Software System
3 Assignments
0 Petitions
Accused Products
Abstract
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).
-
Citations
40 Claims
-
1-20. -20. (canceled)
-
21. A computer-implemented method comprising:
-
receiving software code written in a high-level language, the software code comprising multiple components; compiling the software code to create assembly language code corresponding to the software code; receiving a high-level specification specifying one or more functions performed by the software code; generating a low-level specification based at least in part on the high-level specification; verifying that the assembly language code performs the one or more functions; and providing an indication that the assembly language code has been verified to perform the one or more functions. - View Dependent Claims (22, 23, 24, 25, 26, 27, 28)
-
-
29. A computing device comprising:
-
one or more processors; and one or more memory storage devices to store instructions executable by the one or more processors to perform operations comprising; receiving software code written in a high-level language, the software code comprising multiple components; compiling the software code to create assembly language code corresponding to the software code; receiving a high-level specification specifying one or more functions performed by the software code; generating a low-level specification based at least in part on the high-level specification; verifying that the assembly language code performs the one or more functions; and providing an indication that the assembly language code has been verified to perform the one or more functions. - View Dependent Claims (30, 31, 32, 33, 34, 35)
-
-
36. One or more memory storage devices to store instructions executable by one or more processors to perform operations comprising:
-
receiving software code written in a high-level language, the software code comprising multiple components; compiling the software code to create assembly language code corresponding to the software code; receiving a high-level specification specifying one or more functions performed by the software code; generating a low-level specification based at least in part on the high-level specification; verifying that the assembly language code performs the one or more functions; and providing an indication that the assembly language code has been verified to perform the one or more functions. - View Dependent Claims (37, 38, 39, 40)
-
Specification