Titelaufnahme

Titel
An evaluation of symbol elimination for generating first-order loop invariants / by Ioana Jucu
VerfasserJucu, Ioana
Begutachter / BegutachterinKovacs, Laura
Erschienen2013
UmfangVI, 59 Bl. : graph. Darst.
HochschulschriftWien, Techn. Univ., Dipl.-Arb., 2013
Anmerkung
Zsfassung in dt. Sprache
SpracheEnglisch
DokumenttypDiplomarbeit
URNurn:nbn:at:at-ubtuw:1-75621 Persistent Identifier (URN)
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
An evaluation of symbol elimination for generating first-order loop invariants [0.68 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Deutsch)

Invariant generiert ist ein kritische Problem für Programmen mit Schleife zum Beweisen der Eigenschaften, inclusive die Richtigkeit. Die problem wird schwerer bei hohe Anzhal des Quantoren in die geprüfte Eigenschaft. In diese arbeit wir studiere diese Problem und versuchen combinieren verschieden Methoden für schwarer invariants zu beweisen.

Zusammenfassung (Englisch)

Invariant genereation is a critical problem in proving dierent properties for programs with loops, properties including correctnes. The problem becomes harder with the incresing numbers of quanti ers in the property to be proven. In this paper we study and combine dierent methods of invariant generation in order to obtain stronger properties.