Computer Science – Systems and Control
Scientific paper
2011-07-31
Computer Science
Systems and Control
Scientific paper
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, presence 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-resembling 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.
Feron Eric
Megretski Alexandre
Roozbehani Mardavij
No associations
LandOfFree
Optimization of Lyapunov Invariants in Verification of Software Systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Optimization of Lyapunov Invariants in Verification of Software Systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Optimization of Lyapunov Invariants in Verification of Software Systems will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-703097