Proving Program Termination via Transition Invariants

Kumar, Ramesh

Local TagsRelease HistoryDetailsSummary

Proving Program Termination via Transition Invariants

Kumar, R. (2003). Proving Program Termination via Transition Invariants. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is Released

show all hide all

Basic

show hide

Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-F81B-7 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-F81C-5

Genre: Thesis

Files

show Files

Locators

show

Creators

show

hide

Creators:
Kumar, Ramesh^{1, 2}, Author
Podelski, Andreas², Advisor

Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Content

show

hide

Free keywords: -

Abstract: We can prove termination of C programs by computing 'strong enough' transition invariants by abastract interpretation. In this thesis, we describe basic ingredients for an implementation of this computation. Namely, we show how to extract models form C programs (using GCA tool [7]) and how to construct an abstract domain of transition predicates. Furthermore, we propose a method for 'compacting' a model that improves the running time of the transtion invariant generation algorithm. We implement these ingredients and the proposed optimization, and practically evaluate their effectiveness

Details

show

hide

Language(s): eng - English

Dates: Accepted: 2003Date issued: 2003

Publication Status: Issued

Pages: -

Publishing info: Saarbrücken : Universität des Saarlandes

Table of Contents: -

Rev. Type: -

Identifiers: BibTex Citekey: Kumar2003

Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show