Automata based logics for program verification
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Formal software verification consists in a rigorous analysis of programs using mathematical logic, in order to demonstrat they meet their specification, and ensure with strong confidence in the absence of bugs. The choice of the logical framework to perform the analysis is crucial, and must address two issues: not only must the logic be expressive enough to express the specification and reflect the action of each instruction, but also the logic formalism must be simple enough in order to automate efficiently as much as possible the verification process. In this thesis we will study two logical frameworks and show how to manipulate those. First we will focus on first-order logics over automatic structures, such as Presburger Arithmetics which allows to express properties about integers. We will show that formulas can be effectively represented as automata, and we will detail a generic automata-based algorithn that allow to decide such first-order logics, whose complexity closely matches the hardness of those logics. Then we will present streaming string transducers, which are automata with a finite number of write-only registers and we will inspect their expressiveness. We will present this elegant extension of finite state automata to define string transformations as an intuitive computational model and we will establish their expressive power is precisely express transformations definable by monadic second-order logics
Abstract FR:
La vérification formelle de programmes consiste à raisonner rigoureusement, à l'aide de logiques mathématiques sur des programmes informatiques afin de démontrer leur validité vis-à-vis d'une certaine spécification. Cela permet d'obtenir une très forte assurance d'absence de bug. Le choix du cadre logique dans lequel effectuer la vérification d'un programme est dicté par deux impératifs: la logique doit être suffisamment expressive pour exprimer la spécification voulue et rendre compte de chacune des instructions du programme; et elle doit être suffisamment peu complexe, afin de pouvoir automatiser autant que possible (et en temps raisonable), le processus de vérification. Dans cette thèse, nous étudions deux types de logiques et comment les manipuler pour la vérification formelle. D'abord 1 logique du premier ordre sur les structures automatiques, par exemple l'Arithmétique de Presburger, qui permet d'exprimer des propriétés sur les entiers. Nous montrons qu'elles peuvent être efficacement représentées et manipulées avec des automates, typiquement nous détaillons un algorithme générique basé sur les automates qui permet de décider entre autres l'Arithmétique de Presburger avec une complexité proche de sa difficulté. Ensuite, nous présentons des transducteurs finis avec des registres en écriture seule, et étudions leur pouvoir expressif. Nous verrons qu'ils sont une extension élégante des automates finis pour définir des transformations de mots, étant un modèle calculatoire simple et intuitif, et nous établissons qu'ils permettent d'implémenter les transformations définissables par la logique monadique du second ordre.