Convex optimization proves software correctness

Mardavij Roozbehani, Alexandre Megretski, Eric Feron

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

Abstract

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.
Original languageEnglish (US)
Title of host publicationProceedings of the American Control Conference
Pages1395-1400
Number of pages6
StatePublished - Sep 1 2005
Externally publishedYes

Fingerprint

Dive into the research topics of 'Convex optimization proves software correctness'. Together they form a unique fingerprint.

Cite this