Title: Finding loop invariants using tree grammars
Language: English
Authors: Ebner, Gabriel 
Qualification level: Diploma
Advisor: Hetzl, Stefan 
Issue Date: 2015
Number of Pages: 64
Qualification level: Diploma
Abstract: 
This thesis applies a method for inductive theorem proving based on tree grammars developed by Eberhard and Hetzl to the generation of loop invariants. We consider the verification of simple loops, which do not contain nested loops, and invariants with a single universal quantifier. The verification of this class of programs is reduced to the existing method for inductive proofs, giving an automated method for finding loop invariants. Chapter 1 contains a new exposition of the existing work on tree grammars, culminating in an efficient algorithm to find a minimal grammar covering a given language. Such a minimal grammar consists of productions in a normal form---these normal forms are described using a logic of term algebras. We also investigate the relation to anti-unification. In chapters 2 and 3 we summarize the existing work on proofs and their grammars. The extraction of Herbrand sequents from cut-free proofs is generalized to proofs with universally quantified cuts: there we can extract a totally rigid tree grammar; for proofs with a single induction, we obtain sip grammars. Inverting this extraction allows us introduce cuts, or induction, respectively. The case of inductive proofs and their sip grammars is slightly generalized to allow for the reduction of loop verification problems. In chapters 4 and 5 the verification of loops without nested loops is reduced to the inductive case. This reduction induces a class of grammars; we give an algorithm for efficiently finding a minimal grammar in this class that covers a given language.
Keywords: proof theory; inductive theorem proving; program verification; loop invariant
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-81713
http://hdl.handle.net/20.500.12708/3747
Library ID: AC12260801
Organisation: E104 - Institut für Diskrete Mathematik und Geometrie 
Publication Type: Thesis
Hochschulschrift
Appears in Collections:Thesis

Files in this item:


Page view(s)

22
checked on Jul 11, 2021

Download(s)

58
checked on Jul 11, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.