Loading...
Please wait, while we are loading the content...
Vérification de propriétés LTL sur des programmes C par génération d'annotations
| Content Provider | Semantic Scholar |
|---|---|
| Author | Stouls, Nicolas Groslambert, Julien |
| Copyright Year | 2011 |
| Abstract | Ce travail propose une methode de verification de proprietes temporelles basee sur la generation automatique d'annotations de programmes. Les annotations generees sont ensuite verifiees par des prouveurs automatiques via un calcul de plus faible precondition. Notre contribution vise a optimiser une technique existante de generation d'annotations, afin d'ameliorer l'automatisation de la verification des obligations de preuve produites. Cette approche a ete outillee sous la forme d'un plugin au sein de l'outil Frama-C pour la verification de programmes~C |
| Starting Page | 16 |
| Ending Page | 16 |
| Page Count | 1 |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://perso.citi.insa-lyon.fr/nstouls/Productions/Seminaires/Aorai/2008-10_PFC+ProVal.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |