Skip to Main content Skip to Navigation
Conference papers

Algèbre linéaire pour invariants polynomiaux

Steven de Oliveira 1 Saddek Bensalem 2 Virgile Prévosto 1
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Résumé : Nous présentons dans ce papier une nouvelle technique de génération d'invariants dans le contexte d'un certain type de boucles polynomiales. Notre méthode a l'avantage d'être plus rapide que les méthodes existantes pour des boucles équivalentes et plus simple à implanter car elle repose sur des algorithmes d'algèbre linéaire de complexité polynomiale. Un outil implémentant cette méthode est en cours de développement dans Frama-C, une plate-forme open-source, extensible et collaborative dédiée à l'analyse de programmes C.
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-01391490
Contributor : Steven de Oliveira <>
Submitted on : Thursday, November 3, 2016 - 2:02:38 PM
Last modification on : Thursday, June 3, 2021 - 2:56:02 PM
Long-term archiving on: : Saturday, February 4, 2017 - 1:57:19 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01391490, version 1

Citation

Steven de Oliveira, Saddek Bensalem, Virgile Prévosto. Algèbre linéaire pour invariants polynomiaux. 15èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2016, Besançon, France. pp.61. ⟨hal-01391490⟩

Share

Metrics

Record views

316

Files downloads

119