Proving Program Termination via Transition Invariants

Kumar, Ramesh

Lokale TagsFreigabegeschichteDetailsÜbersicht

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 Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

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

Genre: Hochschulschrift

ausblenden:

Urheber:
Kumar, Ramesh^{1, 2}, Autor
Podelski, Andreas², Ratgeber

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

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

Zusammenfassung: 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