TY - GEN
T1 - Modeling, optimization and computation for software verification
AU - Roozbehani, Mardavij
AU - Feron, Eric
AU - Megrestki, Alexandre
N1 - Generated from Scopus record by KAUST IRTS on 2021-02-18
PY - 2005/1/1
Y1 - 2005/1/1
N2 - 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.
AB - 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.
UR - http://link.springer.com/10.1007/978-3-540-31954-2_39
UR - http://www.scopus.com/inward/record.url?scp=24344460541&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-31954-2_39
DO - 10.1007/978-3-540-31954-2_39
M3 - Conference contribution
SP - 606
EP - 622
BT - Lecture Notes in Computer Science
PB - Springer Verlag
ER -