Modeling, optimization and computation for software verification

Mardavij Roozbehani, Eric Feron, Alexandre Megrestki

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

13 Scopus citations

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.
Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science
PublisherSpringer Verlag
Pages606-622
Number of pages17
DOIs
StatePublished - Jan 1 2005
Externally publishedYes

Fingerprint Dive into the research topics of 'Modeling, optimization and computation for software verification'. Together they form a unique fingerprint.

Cite this