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 -