On model-checking pushdown systems models

On model-checking pushdown systems models

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...

Full description

Bibliographic Details
Main Author: Pommellet, Adrien
Other Authors: Sorbonne Paris Cité
Language:en
Published: 2018
Subjects:
Systèmes à pile
Automates à pile
LTL (Logique Temporelle Linéaire)
Hyper-propriétés
Automate à surpile
Pointeur de pile
Réseaux d'automates à pile synchronisés
Abstraction de Kleene
Model-checking
Pushdown systems
Pushdown automata
LTL ( Linear Temporal Logic)
Hyper-properties
Pushdown systems with an upper stack
Stack pointer
Synchronized dynamic pushdown networks
Kleene abstraction
Online Access:http://www.theses.fr/2018USPCC207/document

Internet

http://www.theses.fr/2018USPCC207/document

Similar Items