Optimization of lyapunov invariants in verification of software systems

Mardavij Roozbehani, Alexandre Megretski, Eric Feron

Research output: Contribution to journalArticlepeer-review

11 Scopus citations

Abstract

The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance specifications. These include but are not limited to absence of overflow, absence of division-by-zero, termination in finite time, absence of dead-code, and certain user-specified assertions. Central to this framework are Lyapunov invariants. These are properly constructed functions of the program variables, and satisfy certain properties-analogous to those of Lyapunov functions-along the execution trace. The search for the invariants can be formulated as a convex optimization problem. If the associated optimization problem is feasible, the result is a certificate for the specification. © 1963-2012 IEEE.
Original languageEnglish (US)
Pages (from-to)696-711
Number of pages16
JournalIEEE Transactions on Automatic Control
Volume58
Issue number3
DOIs
StatePublished - Mar 11 2013
Externally publishedYes

Fingerprint

Dive into the research topics of 'Optimization of lyapunov invariants in verification of software systems'. Together they form a unique fingerprint.

Cite this