TY - GEN
T1 - Convex optimization proves software correctness
AU - Roozbehani, Mardavij
AU - Megretski, Alexandre
AU - Feron, Eric
N1 - Generated from Scopus record by KAUST IRTS on 2021-02-18
PY - 2005/9/1
Y1 - 2005/9/1
N2 - 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. ©2005 AACC.
AB - 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. ©2005 AACC.
UR - http://www.scopus.com/inward/record.url?scp=23944445609&partnerID=8YFLogxK
M3 - Conference contribution
SP - 1395
EP - 1400
BT - Proceedings of the American Control Conference
ER -