Benutzer: Gast  Login
Originaltitel:
Temporal Program Verification and Synthesis as Horn Constraints Solving 
Übersetzter Titel:
Temporale Program Verifikation und Synthese als Horn Klauseln Lösung 
Jahr:
2015 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Rybalchenko, Andrey (Prof. Dr.) 
Gutachter:
Rybalchenko, Andrey (Prof. Dr.); Seidl, Helmut (Prof. Dr.); Rümmer, Philipp (Prof. Dr.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
Horn constraints solving, Program verification, Program synthesis, Games solving 
TU-Systematik:
DAT 500d 
Kurzfassung:
Program verification aims at ensuring a program satisfies a given desirable property. Temporal logics form an important class of specification languages. Advances in dealing with existential temporal properties of programs are not on par with that of universal properties. We propose a Horn constraints based method that can not only formalize declaratively but also solve efficiently various problems in formal methods that involve existential (and universal) temporal properties. We apply our metho...    »
 
Übersetzte Kurzfassung:
Programm Verifikation versucht nachzuweisen, dass ein Programm eine gewünschte Eigenschaft erfüllt. Eine wichtige Klasse von Spezifikationformen in diesem Kontext bilden Temporallogiken. Dennoch sind die Methoden zur Behandlung von existentiellen temporal Eigenschaften nicht so ausgereift wie die zur Behandlung von universellen Eigenschaften. Wir präsentieren eine neuartige Methode basierend auf Horn Klauseln, die nicht nur die Eigenschaften formalisiert sondern auch einen effektiven Ansatz zum...    »
 
Mündliche Prüfung:
21.12.2015 
Dateigröße:
784007 bytes 
Seiten:
141 
Letzte Änderung:
10.06.2016