Modeling, optimization and computation for software verification

Mardavij Roozbehani; Eric Feron; Alexandre Megrestki

doi:10.1007/978-3-540-31954-2_39

Modeling, optimization and computation for software verification

Mardavij Roozbehani, Eric Feron, Alexandre Megrestki

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

15 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 language	English (US)
Title of host publication	Lecture Notes in Computer Science
Publisher	Springer Verlag
Pages	606-622
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-540-31954-2_39
State	Published - Jan 1 2005
Externally published	Yes

Bibliographical note

Generated from Scopus record by KAUST IRTS on 2021-02-18

Access to Document

10.1007/978-3-540-31954-2_39

Cite this

@inproceedings{786dc94a4d7a457a9215a79684e9b276,

title = "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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2005.",

author = "Mardavij Roozbehani and Eric Feron and Alexandre Megrestki",

note = "Generated from Scopus record by KAUST IRTS on 2021-02-18",

year = "2005",

month = jan,

day = "1",

doi = "10.1007/978-3-540-31954-2_39",

language = "English (US)",

pages = "606--622",

booktitle = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

address = "Germany",

}

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 -

Modeling, optimization and computation for software verification

Abstract

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this