Modeling, optimization and computation for software verification

Abstract

Modeling and analysis techniques are presented for real-time, safety-critical software. Software analysis is the task of verifying whether the computer code will execute safely, free of run-time errors. The critical properties that prove safe execution include bounded-ness of variables and termination of the program in finite time. In this paper, dynamical system representations of computer programs along with specific models that are pertinent to analysis via an optimization-based search for system invariants are developed. It is shown that the automatic search for system invariants that establish the desired properties of computer code, can be formulated as a convex optimization problem, such as linear programming, semidefinite programming, and/or sum of squares programming. © Springer-Verlag Berlin Heidelberg 2005.