Ressource documentaire
| Logic-based static analysis for the verification of programs with dynamically allocated data structures (en Anglais) | |||
Droits : © Inria Paris - Rocquencourt Auteur(s) : DRAGOI Cesara 03-12-2015 Description : Software development has reached a complexity level that cannot be handled without the aid of computer assisted methods. It is therefore of the highest importance to have rigorous methods and automated techniques for software verification, allowing to ensure a high degree of reliability and of confidence in their behaviors. In this talk, we present logic-based frameworks for automatic verification of programs manipulating dynamically allocated data-structures. We focus on static analysis techniques, that generate assertions about the program’s reachable states using the algorithmic capabilities of the logic in which the analysis is done. The generated assertions identify which data structures have been allocated, e.g., stacks, queues, and properties of their content and size, characterising the multisets of their elements, or data relations such as order constraints and structures equality. Data-structures are typically implemented in libraries. The verification methodology consists in using static analysis to generate for each method assertions describing the relation between its inputs and outputs, and show that these assertions imply the specification as described in the API’s. Mots-clés libres : évaluation sytème informatique | TECHNIQUE Type : image en mouvement Format : video/x-flv Source(s) : rtmpt://fms2.cerimes.fr:80/vod/fuscia/logic.based.static.analysis.for.the.verification.of.programs.with.dynamically.allocated.data.structures_19677/demie_heure_de_science_03122015_c_dragoi.1.mp4 | ||
Entrepôt d'origine : Canal-u.fr Identifiant : oai:canal-u.fr:19677 Type de ressource : Ressource documentaire | |||
| Exporter au format XML |
Ressource pédagogique
| Logic-based static analysis for the verification of programs with dynamically allocated data structures (en Anglais) | |||||||||
Identifiant de la fiche : 19677 Schéma de la métadonnée : LOMv1.0, LOMFRv1.0 Droits : libre de droits, gratuit Droits réservés à l'éditeur et aux auteurs. © Inria Paris - Rocquencourt Auteur(s) : DRAGOI CESARA Éditeur(s) : INRIA (Institut national de recherche en informatique et automatique) 03-12-2015 Description : Software development has reached a complexity level that cannot be handled without the aid of computer assisted methods. It is therefore of the highest importance to have rigorous methods and automated techniques for software verification, allowing to ensure a high degree of reliability and of confidence in their behaviors. In this talk, we present logic-based frameworks for automatic verification of programs manipulating dynamically allocated data-structures. We focus on static analysis techniques, that generate assertions about the program’s reachable states using the algorithmic capabilities of the logic in which the analysis is done. The generated assertions identify which data structures have been allocated, e.g., stacks, queues, and properties of their content and size, characterising the multisets of their elements, or data relations such as order constraints and structures equality. Data-structures are typically implemented in libraries. The verification methodology consists in using static analysis to generate for each method assertions describing the relation between its inputs and outputs, and show that these assertions imply the specification as described in the API’s. Mots-clés libres : évaluation sytème informatique
| PEDAGOGIQUE Type pédagogique : cours / présentation Niveau : master, doctorat TECHNIQUE Type de contenu : image en mouvement Format : video/x-flv Taille : 2.23 Go Durée d'exécution : 41 minutes 50 secondes RELATIONS Cette ressource fait partie de : | ||||||||
Entrepôt d'origine : Canal-u.fr Identifiant : oai:canal-u.fr:19677 Type de ressource : Ressource pédagogique | |||||||||
| Exporter au format XML |