Interprocedural program analysis using visibly pushdown Kleene algebra
|Advisor:||Ktari, Béchir; Desharnais, Jules|
|Abstract:||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.|
|Document Type:||Thèse de doctorat|
|Open Access Date:||17 April 2018|
|Collection:||Thèses et mémoires|
All documents in CorpusUL are protected by Copyright Act of Canada.