非表示:
キーワード:
-
要旨:
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
