Oméga-Algèbre : théorie et application en vérification de programmes

Authors: Bolduc, Claude
Advisor: Desharnais, Jules
Abstract: Kleene algebra is the algebraic theory of finite automata and regular expressions. Recently, Kozen has proposed a framework based on Kleene algebra with tests (a variant of Kleene algebra) for verifying that a program satisfies a security policy specified by a security automaton. Unfortunately, this approach does not allow to verify liveness properties for reactive programs (programs that execute forever). The goal of this thesis is to extend the framework proposed by Kozen for program verification to remove this limitation. For that, we develop the theory of omega algebra, an extension of Kleene algebra suitable for reasoning about nonterminating executions. The main part of this thesis is about omega algebra. In particular, we show some completeness results about the Horn theory of omega algebra.
Document Type: Mémoire de maîtrise
Issue Date: 2006
Open Access Date: 12 April 2018
Grantor: Université Laval
Collection:Thèses et mémoires

Files in this item:
23728.pdf2.48 MBAdobe PDFView/Open
All documents in CorpusUL are protected by Copyright Act of Canada.