Jucu, I. (2013). An evaluation of symbol elimination for generating first-order loop invariants [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2013.22624
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.
de
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.
en
Additional information:
Abweichender Titel laut Übersetzung der Verfasserin/des Verfassers Zsfassung in dt. Sprache
