PVS linear algebra libraries for verification of control software algorithms in C/ACSL

Heber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre Loïc Garoche, Eric Feron, Gilberto Perez, Pablo Ascariz

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

29 Scopus citations


The problem of ensuring control software properties hold on their actual implementation is rarely tackled. While stability proofs are widely used on models, they are never carried to the code. Using program verification techniques requires express these properties at the level of the code but also to have theorem provers that can manipulate the proof elements. We propose to address this challenge by following two phases: first we introduce a way to express stability proofs as C code annotations; second, we propose a PVS linear algebra library that is able to manipulate quadratic invariants, i.e., ellipsoids. Our framework achieves the translation of stability properties expressed on the code to the representation of an associated proof obligation (PO) in PVS. Our library allows us to discharge these POs within PVS. © 2012 Springer-Verlag.
Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Number of pages15
StatePublished - Apr 11 2012
Externally publishedYes

Bibliographical note

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


Dive into the research topics of 'PVS linear algebra libraries for verification of control software algorithms in C/ACSL'. Together they form a unique fingerprint.

Cite this