Les analyses interprocédurales automatiques de programmes qui sont basées sur des
théories mathématiques rigoureuses sont complexes à réaliser, mais elles sont d'excellents
outils pour augmenter notre conance envers les comportements possibles d'un
programme. Les méthodes classiques pour réaliser ces analyses sont l'analyse de modè-
les, l'interprétation abstraite et la démonstration automatique de théorèmes. La base
d'un démonstrateur automatique de théorèmes est une logique ou une algèbre et le
choix de celle-ci a un impact sur la complexité de trouver une preuve pour un théorème
donné.
Cette dissertation développe un formalisme algébrique concis pouvant être utilisé en
démonstration automatique de théorèmes. Ce formalisme est appellé algèbre de Kleene
à pile visible. Cette dissertation explique comment ce formalisme peut être utilisé
pour réaliser des analyses interprocédurales de programmes, comme des vérications
formelles et des vérications d'optimisations efectuées par des compilateurs. Cette
dissertation apporte aussi des preuves que ces analyses pourraient être automatisées.
L'algèbre de Kleene à pile visible est une extension de l'algèbre de Kleene, un excellent
formalisme pour réaliser des analyses intraprocédurales de programmes. En
bref, l'algèbre de Kleene est la théorie algébrique des automates nis et des expressions
régulières. Donc, cette algèbre à elle seule n'est pas appropriée pour faire des analyses
interprocédurales de programmes car la puissance des langages non contextuels est souvent
nécessaire pour représenter le lot de contrôle d'un tel programme. L'algèbre de
Kleene à pile visible étend celle-ci en lui ajoutant une famille d'opérateurs de plus petit
point xe qui est basée sur une restriction des grammaires non contextuelles. En fait,
cette algèbre axiomatise exactement la théorie équationnelle des langages à pile visibles.
Ces langages sont une sous-classe des langages non contextuels et ont été dénis par
Alur et Madhusudan pour faire de l'analyse de modèles. La complexité résultante de
la théorie équationnelle de l'algèbre proposée est EXPTIME-complète. / Automatic interprocedural program analyses based on rigorous mathematical theories
are complex to do, but they are great tools to increase our condence in the behaviour
of a program. Classical ways of doing them is either by model checking, by abstract
interpretation or by automated theorem proving. The basis of an automated theorem
prover is a logic or an algebra and the choice of this basis will have an impact in the
complexity of nding a proof for a given theorem.
This dissertation develops a lightweight algebraic formalism for the automated theorem
proving approach. This formalism is called visibly pushdown Kleene algebra. This
dissertation explains how to do some interprocedural program analyses, like formal veri
cation and verication of compiler optimizations, with this formalism. Evidence is
provided that the analyses can be automated.
The proposed algebraic formalism is an extension of Kleene algebra, a formalism for
doing intraprocedural program analyses. In a nutshell, Kleene algebra is the algebraic
theory of nite automata and regular expressions. So, Kleene algebra alone is not
well suited to do interprocedural program analyses, where the power of context-free
languages is often needed to represent the control flow of a program. Visibly pushdown
Kleene algebra extends Kleene algebra by adding a family of implicit least xed point
operators based on a restriction of context-free grammars. In fact, visibly pushdown
Kleene algebra axiomatises exactly the equational theory of visibly pushdown languages.
Visibly pushdown languages are a subclass of context-free languages dened by Alur and
Madhusudan in the model checking framework to model check interprocedural programs
while remaining decidable. The resulting complexity of the equational theory of visibly
pushdown Kleene algebra is EXPTIME-complete whereas that of Kleene algebra is
PSPACE-complete.
| Identifer | oai:union.ndltd.org:LACETR/oai:collectionscanada.gc.ca:QQLA.2011/28229 |
| Date | 06 1900 |
| Creators | Bolduc, Claude |
| Contributors | Ktari, Béchir, Desharnais, Jules |
| Publisher | Université Laval |
| Source Sets | Library and Archives Canada ETDs Repository / Centre d'archives des thèses électroniques de Bibliothèque et Archives Canada |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation |
| Format | application/pdf |
| Rights | © Claude Bolduc, 2011 |
Page generated in 0.0273 seconds