Interprocedural program analysis using visibly pushdown Kleene algebra

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