Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming

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

Abstract

In order to verify semialgebraic programs, we automatize the Floyd/Naur/Hoare proof method. The main task is to automatically infer valid invariants and rank functions. First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd/Naur/Hoare verification conditions is handled by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using semidefinite programming solvers. This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal/dual interior point methods generalizing those well-known in linear programming to convex optimization. The framework is applied to invariance and termination proof of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science
EditorsR. Cousot
Pages1-24
Number of pages24
Volume3385
StatePublished - 2005
Event6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2005 - Paris, France
Duration: Jan 17 2005Jan 19 2005

Other

Other6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2005
CountryFrance
CityParis
Period1/17/051/19/05

Fingerprint

Invariance
Polynomials
Convex optimization
Linear programming
Semantics

Keywords

  • Bilinear matrix inequality (BMI)
  • Convex optimization
  • Invariance
  • Lagrangian relaxation
  • Linear matrix inequality (LMI)
  • Liveness
  • Parametric abstraction
  • Polynomial optimization
  • Proof
  • Rank function
  • S-procedure
  • Safety
  • Semidefinite programming

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. / Cousot, Patrick.

Lecture Notes in Computer Science. ed. / R. Cousot. Vol. 3385 2005. p. 1-24.

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

Cousot, P 2005, Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. in R Cousot (ed.), Lecture Notes in Computer Science. vol. 3385, pp. 1-24, 6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2005, Paris, France, 1/17/05.
@inproceedings{261c50acd0674b1cba15d58d28361fe8,
title = "Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming",
abstract = "In order to verify semialgebraic programs, we automatize the Floyd/Naur/Hoare proof method. The main task is to automatically infer valid invariants and rank functions. First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd/Naur/Hoare verification conditions is handled by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using semidefinite programming solvers. This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal/dual interior point methods generalizing those well-known in linear programming to convex optimization. The framework is applied to invariance and termination proof of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties.",
keywords = "Bilinear matrix inequality (BMI), Convex optimization, Invariance, Lagrangian relaxation, Linear matrix inequality (LMI), Liveness, Parametric abstraction, Polynomial optimization, Proof, Rank function, S-procedure, Safety, Semidefinite programming",
author = "Patrick Cousot",
year = "2005",
language = "English (US)",
volume = "3385",
pages = "1--24",
editor = "R. Cousot",
booktitle = "Lecture Notes in Computer Science",

}

TY - GEN

T1 - Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming

AU - Cousot, Patrick

PY - 2005

Y1 - 2005

N2 - In order to verify semialgebraic programs, we automatize the Floyd/Naur/Hoare proof method. The main task is to automatically infer valid invariants and rank functions. First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd/Naur/Hoare verification conditions is handled by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using semidefinite programming solvers. This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal/dual interior point methods generalizing those well-known in linear programming to convex optimization. The framework is applied to invariance and termination proof of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties.

AB - In order to verify semialgebraic programs, we automatize the Floyd/Naur/Hoare proof method. The main task is to automatically infer valid invariants and rank functions. First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd/Naur/Hoare verification conditions is handled by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using semidefinite programming solvers. This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal/dual interior point methods generalizing those well-known in linear programming to convex optimization. The framework is applied to invariance and termination proof of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties.

KW - Bilinear matrix inequality (BMI)

KW - Convex optimization

KW - Invariance

KW - Lagrangian relaxation

KW - Linear matrix inequality (LMI)

KW - Liveness

KW - Parametric abstraction

KW - Polynomial optimization

KW - Proof

KW - Rank function

KW - S-procedure

KW - Safety

KW - Semidefinite programming

UR - http://www.scopus.com/inward/record.url?scp=24144488686&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=24144488686&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:24144488686

VL - 3385

SP - 1

EP - 24

BT - Lecture Notes in Computer Science

A2 - Cousot, R.

ER -