Convex optimization proves software correctness

This paper concerns analysis of real-time, safety-critical, embedded software. Software analysis is expected to verify whether the computer code will execute safely, free of run-time errors. The main properties to be analyzed to prove or disprove safe execution include boundedness of all variables and termination of the program in finite-time. Herein the concepts of Lyapunov invariance and associated computational procedures are brought within the context of software analysis. Dynamical system representations of software systems along with specific models that are suitable for analysis via Lyapunov-like functions are developed. General forms for the Lyapunov-like invariants are then constructed in a way to certify the desired properties. Convex optimization methods such as linear programming and/or semidefinite programming are then employed for finding appropriate functions that fit into these general forms and therefore, automatically establish the key properties of software.