Return to search

Abstract lattices for the verification of systèmes with stacks and queues

L'analyse des systèmes communiquant par file a fait l'objet d'études scientifiques nombreuses mais qui n'ont pu offrir des solutions totalement satisfaisantes. Nous proposons d'aborder ce problème dans le cadre de l'interprétation abstraite, en définissant des treillis abstraits adaptés à ce type de systèmes. Nous considérons d'abord le cas où les messages échangés sont assimilables à un alphabet fini, puis nous nous attaquons au cas, plus difficile, des messages portant des valeurs entières ou réelles. Ce problème nous amène à définir et à étudier un nouveau type d'automate, les automates de treillis. Ces automates de treillis peuvent également être utilisés pour l'analyses des programmes utilisant une pile d'appels.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00424552
Date02 July 2008
CreatorsLe Gall, Tristan
PublisherUniversité Rennes 1
Source SetsCCSD theses-EN-ligne, France
LanguageEnglish
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0017 seconds