Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Cette thèse introduit différentes méthodes de vérification (ou model-checking) sur des modèles de systèmes à pile. En effet, les systèmes à pile (pushdown systems) modélisent naturellement les programmes séquentiels grâce à une pile infinie qui peut simuler la pile d'appel du logiciel. La première partie de cette thèse se concentre sur la vérification sur des systèmes à pile de la logique HyperLTL, qui enrichit la logique temporelle LTL de quantificateurs universels et existentiels sur des variables de chemin. Il a été prouvé que le problème de la vérification de la logique HyperLTL sur des systèmes d'états finis est décidable ; nous montrons que ce problème est en revanche indécidable pour les systèmes à pile ainsi que pour la sous-classe des systèmes à pile visibles (visibly pushdown systems). Nous introduisons donc des algorithmes d'approximation de ce problème, que nous appliquons ensuite à la vérification de politiques de sécurité. Dans la seconde partie de cette thèse, dans la mesure où la représentation de la pile d'appel par les systèmes à pile est approximative, nous introduisons les systèmes à surpile (pushdown systems with an upper stack) ; dans ce modèle, les symboles retirés de la pile d'appel persistent dans la zone mémoire au dessus du pointeur de pile, et peuvent être plus tard écrasés par des appels sur la pile. Nous montrons que les ensembles de successeurs post* et de prédécesseurs pre* d'un ensemble régulier de configurations ne sont pas réguliers pour ce modèle, mais que post* est toutefois contextuel (context-sensitive), et que l'on peut ainsi décider de l'accessibilité d'une configuration. Nous introduisons donc des algorithmes de sur-approximation de post* et de sous-approximation de pre*, que nous appliquons à la détection de débordements de pile et de manipulations nuisibles du pointeur de pile. Enfin, dans le but d'analyser des programmes avec plusieurs fils d'exécution, nous introduisons le modèle des réseaux à piles dynamiques synchronisés (synchronized dynamic pushdown networks), ...