TY - GEN

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

AU - Herencia-Zapana, Heber

AU - Jobredeaux, Romain

AU - Owre, Sam

AU - Garoche, Pierre Loïc

AU - Feron, Eric

AU - Perez, Gilberto

AU - Ascariz, Pablo

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

PY - 2012/4/11

Y1 - 2012/4/11

N2 - 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.

AB - 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.

UR - http://link.springer.com/10.1007/978-3-642-28891-3_15

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

U2 - 10.1007/978-3-642-28891-3_15

DO - 10.1007/978-3-642-28891-3_15

M3 - Conference contribution

SN - 9783642288906

SP - 147

EP - 161

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -